Skip to content

Commit aaf5a8a

Browse files
elierichaeliericha
committed
Merge branch 'topic/spark-shortcuts' into 'master'
Use commands for shortcuts that wrap tasks See merge request eng/ide/ada_language_server!1670
2 parents 88bc8d1 + 2fba6e1 commit aaf5a8a

File tree

3 files changed

+66
-12
lines changed

3 files changed

+66
-12
lines changed

‎integration/vscode/ada/package.json

Lines changed: 24 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -776,6 +776,26 @@
776776
"title": "Ada: Build and run last used main",
777777
"icon": "$(run)",
778778
"when": "ADA_PROJECT_CONTEXT"
779+
},
780+
{
781+
"command": "ada.spark.tasks.proveFile",
782+
"title": "spark: Prove file (task wrapper)",
783+
"when": "editorLangId == ada && editorTextFocus"
784+
},
785+
{
786+
"command": "ada.spark.tasks.proveSubprogram",
787+
"title": "spark: Prove subprogram (task wrapper)",
788+
"when": "editorLangId == ada && editorTextFocus"
789+
},
790+
{
791+
"command": "ada.spark.tasks.proveSelectedRegion",
792+
"title": "spark: Prove selected region (task wrapper)",
793+
"when": "editorLangId == ada && editorTextFocus"
794+
},
795+
{
796+
"command": "ada.spark.tasks.proveLine",
797+
"title": "spark: Prove line (task wrapper)",
798+
"when": "editorLangId == ada && editorTextFocus"
779799
}
780800
],
781801
"keybindings": [
@@ -790,26 +810,22 @@
790810
"when": "editorLangId == ada && editorTextFocus"
791811
},
792812
{
793-
"command": "workbench.action.tasks.runTask",
794-
"args": "spark: Prove file",
813+
"command": "ada.spark.tasks.proveFile",
795814
"key": "meta+y meta+f",
796815
"when": "editorLangId == ada && editorTextFocus"
797816
},
798817
{
799-
"command": "workbench.action.tasks.runTask",
800-
"args": "spark: Prove subprogram",
818+
"command": "ada.spark.tasks.proveSubprogram",
801819
"key": "meta+y meta+s",
802820
"when": "editorLangId == ada && editorTextFocus"
803821
},
804822
{
805-
"command": "workbench.action.tasks.runTask",
806-
"args": "spark: Prove selected region",
823+
"command": "ada.spark.tasks.proveSelectedRegion",
807824
"key": "meta+y meta+r",
808825
"when": "editorLangId == ada && editorTextFocus"
809826
},
810827
{
811-
"command": "workbench.action.tasks.runTask",
812-
"args": "spark: Prove line",
828+
"command": "ada.spark.tasks.proveLine",
813829
"key": "meta+y meta+l",
814830
"when": "editorLangId == ada && editorTextFocus"
815831
}

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

Lines changed: 36 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@ import assert from 'assert';
22
import { existsSync } from 'fs';
33
import { basename } from 'path';
44
import * as vscode from 'vscode';
5-
import { SymbolKind } from 'vscode';
5+
import { SymbolKind, commands } from 'vscode';
66
import { Disposable } from 'vscode-jsonrpc';
77
import { ExecuteCommandRequest } from 'vscode-languageclient';
88
import { ExtensionState } from './ExtensionState';
@@ -11,6 +11,9 @@ import { adaExtState, logger, mainOutputChannel } from './extension';
1111
import { findAdaMain, getProjectFileRelPath, getSymbols } from './helpers';
1212
import {
1313
SimpleTaskDef,
14+
TASK_PROVE_FILE_PLAIN_NAME,
15+
TASK_PROVE_LINE_PLAIN_NAME,
16+
TASK_PROVE_REGION_PLAIN_NAME,
1417
TASK_PROVE_SUPB_PLAIN_NAME,
1518
TASK_TYPE_SPARK,
1619
findBuildAndRunTask,
@@ -140,7 +143,39 @@ export function registerCommands(context: vscode.ExtensionContext, clients: Exte
140143
context.subscriptions.push(
141144
vscode.commands.registerCommand(CMD_SPARK_PROVE_SUBP, sparkProveSubprogram)
142145
);
146+
147+
registerTaskWrappers(context);
148+
}
149+
150+
/**
151+
* The following commands are wrappers around VS Code tasks that allow setting
152+
* key shortcuts to the wrapped tasks. Technically it is possible to set
153+
* shortcuts directly on the `workbench.action.tasks.runTask` command with the
154+
* target task as a command argument, however in several places the UI doesn't
155+
* take into consideration the command argument, and thus it becomes impossible
156+
* to distinguish the different tasks, and worse, our shortcut becomes
157+
* displayed for the vanilla `Run Task` command.
158+
*
159+
* To avoid all that, we provide these commands as wrappers.
160+
*/
161+
function registerTaskWrappers(context: vscode.ExtensionContext) {
162+
const sparkTaskWrappers: { [cmdId: string]: string } = {
163+
'ada.spark.tasks.proveFile': `${TASK_TYPE_SPARK}: ${TASK_PROVE_FILE_PLAIN_NAME}`,
164+
'ada.spark.tasks.proveSubprogram': `${TASK_TYPE_SPARK}: ${TASK_PROVE_SUPB_PLAIN_NAME}`,
165+
// eslint-disable-next-line max-len
166+
'ada.spark.tasks.proveSelectedRegion': `${TASK_TYPE_SPARK}: ${TASK_PROVE_REGION_PLAIN_NAME}`,
167+
'ada.spark.tasks.proveLine': `${TASK_TYPE_SPARK}: ${TASK_PROVE_LINE_PLAIN_NAME}`,
168+
};
169+
for (const cmdId of Object.keys(sparkTaskWrappers)) {
170+
const taskId = sparkTaskWrappers[cmdId];
171+
context.subscriptions.push(
172+
commands.registerCommand(cmdId, () =>
173+
commands.executeCommand('workbench.action.tasks.runTask', taskId)
174+
)
175+
);
176+
}
143177
}
178+
144179
/**
145180
* Add a subprogram box above the subprogram enclosing the cursor's position, if any.
146181
*

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

Lines changed: 6 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -87,6 +87,9 @@ const TASK_CLEAN_PROJECT = {
8787
};
8888

8989
export const TASK_PROVE_SUPB_PLAIN_NAME = 'Prove subprogram';
90+
export const TASK_PROVE_REGION_PLAIN_NAME = 'Prove selected region';
91+
export const TASK_PROVE_LINE_PLAIN_NAME = 'Prove line';
92+
export const TASK_PROVE_FILE_PLAIN_NAME = 'Prove file';
9093

9194
/**
9295
* Predefined tasks offered by the extension. Both 'ada' and 'spark' tasks are
@@ -289,7 +292,7 @@ const predefinedTasks: PredefinedTask[] = [
289292
problemMatchers: DEFAULT_PROBLEM_MATCHER,
290293
},
291294
{
292-
label: 'Prove file',
295+
label: TASK_PROVE_FILE_PLAIN_NAME,
293296
taskDef: {
294297
type: TASK_TYPE_SPARK,
295298
command: 'gnatprove',
@@ -320,7 +323,7 @@ const predefinedTasks: PredefinedTask[] = [
320323
problemMatchers: DEFAULT_PROBLEM_MATCHER,
321324
},
322325
{
323-
label: 'Prove selected region',
326+
label: TASK_PROVE_REGION_PLAIN_NAME,
324327
taskDef: {
325328
type: TASK_TYPE_SPARK,
326329
command: 'gnatprove',
@@ -337,7 +340,7 @@ const predefinedTasks: PredefinedTask[] = [
337340
problemMatchers: DEFAULT_PROBLEM_MATCHER,
338341
},
339342
{
340-
label: 'Prove line',
343+
label: TASK_PROVE_LINE_PLAIN_NAME,
341344
taskDef: {
342345
type: TASK_TYPE_SPARK,
343346
command: 'gnatprove',

0 commit comments

Comments
 (0)