Skip to content

Commit c1c5001

Browse files
elierichaeliericha
committed
Use GNATprove option picker with all SPARK tasks
And remove circular importing between some modules
1 parent b9bb55f commit c1c5001

File tree

8 files changed

+145
-117
lines changed

8 files changed

+145
-117
lines changed

‎integration/vscode/ada/src/AdaCodeLensProvider.ts‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -16,8 +16,8 @@ import {
1616
CMD_BUILD_AND_DEBUG_MAIN,
1717
CMD_BUILD_AND_RUN_GNATEMULATOR,
1818
CMD_BUILD_AND_RUN_MAIN,
19-
CMD_SPARK_PROVE_SUBP,
20-
} from './commands';
19+
CMD_SPARK_PROVE_SUBP
20+
} from './constants';
2121
import { envHasExec, getSymbols } from './helpers';
2222
import { adaExtState } from './extension';
2323

‎integration/vscode/ada/src/ExtensionState.ts‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -13,8 +13,8 @@ import {
1313
CMD_RESTART_LANG_SERVERS,
1414
CMD_SHOW_ADA_LS_OUTPUT,
1515
CMD_SHOW_EXTENSION_LOGS,
16-
CMD_SHOW_GPR_LS_OUTPUT,
17-
} from './commands';
16+
CMD_SHOW_GPR_LS_OUTPUT
17+
} from './constants';
1818
import { AdaInitialDebugConfigProvider, initializeDebugging } from './debugConfigProvider';
1919
import { logger } from './extension';
2020
import { GnatTaskProvider } from './gnatTaskProvider';

‎integration/vscode/ada/src/alsExecuteCommand.ts‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -40,7 +40,7 @@ import {
4040
ReplaceTypeCommandArgs,
4141
} from './refactoring/alsReplaceTypeCommand';
4242
import { adaExtState } from './extension';
43-
import { CMD_RELOAD_PROJECT } from './commands';
43+
import { CMD_RELOAD_PROJECT } from './constants';
4444

4545
/**
4646
* Type alias for a function that intercepts a command and executes it by return a promise that

‎integration/vscode/ada/src/commands.ts‎

Lines changed: 16 additions & 83 deletions
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,22 @@ import { Disposable } from 'vscode-jsonrpc';
77
import { ExecuteCommandRequest } from 'vscode-languageclient';
88
import { ALSSourceDirDescription, ExtensionState } from './ExtensionState';
99
import { startVisualize } from './alsVisualizer';
10+
import {
11+
CMD_BUILD_AND_DEBUG_GNATEMULATOR,
12+
CMD_BUILD_AND_DEBUG_MAIN,
13+
CMD_BUILD_AND_RUN_GNATEMULATOR,
14+
CMD_BUILD_AND_RUN_MAIN,
15+
CMD_GET_PROJECT_FILE,
16+
CMD_GPR_PROJECT_ARGS,
17+
CMD_RESTART_LANG_SERVERS,
18+
CMD_SHOW_ADA_LS_OUTPUT,
19+
CMD_SHOW_EXTENSION_LOGS,
20+
CMD_SHOW_GPR_LS_OUTPUT,
21+
CMD_SPARK_ASK_OPTIONS,
22+
CMD_SPARK_LIMIT_REGION_ARG,
23+
CMD_SPARK_LIMIT_SUBP_ARG,
24+
CMD_SPARK_PROVE_SUBP,
25+
} from './constants';
1026
import { AdaConfig, getOrAskForProgram, initializeConfig } from './debugConfigProvider';
1127
import { adaExtState, logger, mainOutputChannel } from './extension';
1228
import { loadGnatCoverageReport } from './gnattest';
@@ -33,89 +49,6 @@ import {
3349
import { Hierarchy } from './visualizerTypes';
3450
import { createHelloWorldProject, walkthroughStartDebugging } from './walkthrough';
3551

36-
/**
37-
* Identifier for a hidden command used for building and running a project main.
38-
* The command accepts a parameter which is the URI of the main source file.
39-
* It is triggered by CodeLenses provided by the extension.
40-
*
41-
* @see {@link buildAndRunSpecifiedMain}
42-
*/
43-
export const CMD_BUILD_AND_RUN_MAIN = 'ada.buildAndRunMain';
44-
45-
/**
46-
* Identifier for a hidden command used for building and debugging a project main.
47-
* The command accepts a parameter which is the URI of the main source file.
48-
* It is triggered by CodeLenses provided by the extension.
49-
*
50-
* @see {@link buildAndDebugSpecifiedMain}
51-
*/
52-
export const CMD_BUILD_AND_DEBUG_MAIN = 'ada.buildAndDebugMain';
53-
54-
/**
55-
* Identifier for a hidden command used for building and running a project main,
56-
* using GNATemulator.
57-
* The command accepts a parameter which is the URI of the main source file.
58-
* It is triggered by CodeLenses provided by the extension.
59-
*
60-
* @see {@link buildAndRunMainWithGNATemulator}
61-
*/
62-
export const CMD_BUILD_AND_RUN_GNATEMULATOR = 'ada.buildAndRunGNATemulator';
63-
64-
/**
65-
* Identifier for a hidden command used for building and debugging a project main,
66-
* using GNATemulator.
67-
* The command accepts a parameter which is the URI of the main source file.
68-
* It is triggered by CodeLenses provided by the extension.
69-
*
70-
* @see {@link buildAndDebugSpecifiedMain}
71-
*/
72-
export const CMD_BUILD_AND_DEBUG_GNATEMULATOR = 'ada.buildAndDebugGNATemulator';
73-
74-
/**
75-
* Identifier for a hidden command that returns an array of strings constituting
76-
* the -P and -X project and scenario arguments.
77-
*/
78-
export const CMD_GPR_PROJECT_ARGS = 'ada.gprProjectArgs';
79-
80-
/**
81-
* Identifier for a hidden command that returns a string referencing the current
82-
* project. That string is either `"$\{config:ada.projectFile\}"` if that
83-
* setting is configured, or otherwise the full path to the project file
84-
* returned from a query to the
85-
*/
86-
export const CMD_GET_PROJECT_FILE = 'ada.getProjectFile';
87-
88-
export const CMD_SPARK_LIMIT_SUBP_ARG = 'ada.spark.limitSubpArg';
89-
export const CMD_SPARK_LIMIT_REGION_ARG = 'ada.spark.limitRegionArg';
90-
export const CMD_SPARK_PROVE_SUBP = 'ada.spark.proveSubprogram';
91-
const CMD_SPARK_ASK_OPTIONS = 'ada.spark.askGNATproveOptions';
92-
93-
/**
94-
* Identifier for the command that shows the extension's output in the Output panel.
95-
*/
96-
export const CMD_SHOW_EXTENSION_LOGS = 'ada.showExtensionOutput';
97-
98-
/**
99-
* Identifier for the command that shows the output of the ALS for Ada in the Output panel.
100-
*/
101-
export const CMD_SHOW_ADA_LS_OUTPUT = 'ada.showAdaLSOutput';
102-
103-
/**
104-
* Identifier for the command that shows the output of the ALS for GPR in the Output panel.
105-
*/
106-
export const CMD_SHOW_GPR_LS_OUTPUT = 'ada.showGprLSOutput';
107-
108-
/**
109-
* Identifier for the command that reloads the currently loaded project on server-side.
110-
*/
111-
export const CMD_RELOAD_PROJECT = 'als-reload-project';
112-
113-
/**
114-
* Identifier for the command that restarts all the language servers spawned by the extension
115-
* (Ada and GPR).
116-
*/
117-
export const CMD_RESTART_LANG_SERVERS = 'ada.restartLanguageServers';
118-
11952
export function registerCommands(context: vscode.ExtensionContext, clients: ExtensionState) {
12053
context.subscriptions.push(
12154
vscode.commands.registerCommand(CMD_RESTART_LANG_SERVERS, restartLanguageServers),

‎integration/vscode/ada/src/constants.ts‎

Lines changed: 83 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,83 @@
1+
/**
2+
* Identifier for a hidden command used for building and running a project main.
3+
* The command accepts a parameter which is the URI of the main source file.
4+
* It is triggered by CodeLenses provided by the extension.
5+
*
6+
* @see {@link buildAndRunSpecifiedMain}
7+
*/
8+
9+
export const CMD_BUILD_AND_RUN_MAIN = 'ada.buildAndRunMain';
10+
/**
11+
* Identifier for a hidden command used for building and debugging a project main.
12+
* The command accepts a parameter which is the URI of the main source file.
13+
* It is triggered by CodeLenses provided by the extension.
14+
*
15+
* @see {@link buildAndDebugSpecifiedMain}
16+
*/
17+
18+
export const CMD_BUILD_AND_DEBUG_MAIN = 'ada.buildAndDebugMain';
19+
/**
20+
* Identifier for a hidden command used for building and running a project main,
21+
* using GNATemulator.
22+
* The command accepts a parameter which is the URI of the main source file.
23+
* It is triggered by CodeLenses provided by the extension.
24+
*
25+
* @see {@link buildAndRunMainWithGNATemulator}
26+
*/
27+
28+
export const CMD_BUILD_AND_RUN_GNATEMULATOR = 'ada.buildAndRunGNATemulator';
29+
/**
30+
* Identifier for a hidden command used for building and debugging a project main,
31+
* using GNATemulator.
32+
* The command accepts a parameter which is the URI of the main source file.
33+
* It is triggered by CodeLenses provided by the extension.
34+
*
35+
* @see {@link buildAndDebugSpecifiedMain}
36+
*/
37+
38+
export const CMD_BUILD_AND_DEBUG_GNATEMULATOR = 'ada.buildAndDebugGNATemulator';
39+
/**
40+
* Identifier for a hidden command that returns an array of strings constituting
41+
* the -P and -X project and scenario arguments.
42+
*/
43+
44+
export const CMD_GPR_PROJECT_ARGS = 'ada.gprProjectArgs';
45+
/**
46+
* Identifier for a hidden command that returns a string referencing the current
47+
* project. That string is either `"$\{config:ada.projectFile\}"` if that
48+
* setting is configured, or otherwise the full path to the project file
49+
* returned from a query to the
50+
*/
51+
52+
export const CMD_GET_PROJECT_FILE = 'ada.getProjectFile';
53+
54+
export const CMD_SPARK_LIMIT_SUBP_ARG = 'ada.spark.limitSubpArg';
55+
export const CMD_SPARK_LIMIT_REGION_ARG = 'ada.spark.limitRegionArg';
56+
export const CMD_SPARK_PROVE_SUBP = 'ada.spark.proveSubprogram';
57+
export const CMD_SPARK_ASK_OPTIONS = 'ada.spark.askGNATproveOptions';
58+
/**
59+
* Identifier for the command that shows the extension's output in the Output panel.
60+
*/
61+
62+
export const CMD_SHOW_EXTENSION_LOGS = 'ada.showExtensionOutput';
63+
/**
64+
* Identifier for the command that shows the output of the ALS for Ada in the Output panel.
65+
*/
66+
67+
export const CMD_SHOW_ADA_LS_OUTPUT = 'ada.showAdaLSOutput';
68+
/**
69+
* Identifier for the command that shows the output of the ALS for GPR in the Output panel.
70+
*/
71+
72+
export const CMD_SHOW_GPR_LS_OUTPUT = 'ada.showGprLSOutput';
73+
/**
74+
* Identifier for the command that reloads the currently loaded project on server-side.
75+
*/
76+
77+
export const CMD_RELOAD_PROJECT = 'als-reload-project';
78+
/**
79+
* Identifier for the command that restarts all the language servers spawned by the extension
80+
* (Ada and GPR).
81+
*/
82+
83+
export const CMD_RESTART_LANG_SERVERS = 'ada.restartLanguageServers';

0 commit comments

Comments
 (0)