Skip to content

Commit 7e1255d

Browse files
committed
Merge branch 'wip/moy-176-spark' into 'master'
Improvements of the SPARK support See merge request eng/ide/ada_language_server!1198
2 parents 853e902 + 78b4045 commit 7e1255d

File tree

2 files changed

+14
-7
lines changed

2 files changed

+14
-7
lines changed

README.md

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -158,6 +158,7 @@ The extension includes a task provider. It provides the following "auto-detected
158158
* "ada: Prove subprogram" - launch `gnatprove` on the current subprogram in the current editor
159159
* "ada: Prove selected region" - launch `gnatprove` on the selected region in the current editor
160160
* "ada: Prove line" - launch `gnatprove` on the cursor line in the current editor
161+
* "ada: Clean project for proof" - launch `gnatprove` on the current GPR project to clean proof artefacts
161162

162163
You can bind keyboard shortcuts to them by adding to the `keybindings.json` file:
163164

integration/vscode/ada/src/gnatTaskProvider.ts

Lines changed: 13 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -94,44 +94,50 @@ const getGnatArgs = (args: string[]): string[] => {
9494
* Map of known tasks/tools indexed by a string/taskKind
9595
*/
9696
const knownTaskKinds: { [id: string]: TaskProperties } = {
97+
cleanProjectForProof: {
98+
command: getGnatArgs(['gnatprove', '--clean']),
99+
extra: undefined,
100+
title: 'Clean project for proof',
101+
},
97102
examineProject: {
98-
command: getGnatArgs(['gnatprove', '--mode=flow']),
103+
command: getGnatArgs(['gnatprove', '-j0', '--mode=flow']),
99104
extra: undefined,
100105
title: 'Examine project',
101106
},
102107
examineFile: {
103-
command: getGnatArgs(['gnatprove', '--mode=flow', '-u', '${fileBasename}']),
108+
command: getGnatArgs(['gnatprove', '-j0', '--mode=flow', '-u', '${fileBasename}']),
104109
extra: undefined,
105110
title: 'Examine file',
106111
},
107112
examineSubprogram: {
108-
command: ['gnatprove', '--mode=flow'],
113+
command: ['gnatprove', '-j0', '--mode=flow'],
109114
extra: limitSubp,
110115
title: 'Examine subprogram',
111116
},
112117
proveProject: {
113-
command: getGnatArgs(['gnatprove']),
118+
command: getGnatArgs(['gnatprove', '-j0']),
114119
extra: undefined,
115120
title: 'Prove project',
116121
},
117122
proveFile: {
118-
command: getGnatArgs(['gnatprove', '-u', '${fileBasename}']),
123+
command: getGnatArgs(['gnatprove', '-j0', '-u', '${fileBasename}']),
119124
extra: undefined,
120125
title: 'Prove file',
121126
},
122127
proveSubprogram: {
123-
command: ['gnatprove'],
128+
command: ['gnatprove', '-j0'],
124129
extra: limitSubp,
125130
title: 'Prove subprogram',
126131
},
127132
proveRegion: {
128-
command: ['gnatprove', '-u', '${fileBasename}'],
133+
command: ['gnatprove', '-j0', '-u', '${fileBasename}'],
129134
extra: limitRegion,
130135
title: 'Prove selected region',
131136
},
132137
proveLine: {
133138
command: getGnatArgs([
134139
'gnatprove',
140+
'-j0',
135141
'-u',
136142
'${fileBasename}',
137143
'--limit-line=${fileBasename}:${lineNumber}',

0 commit comments

Comments
 (0)