Skip to content

Commit ae70b16

Browse files
elierichaeliericha
committed
Create a multi-step picker for SPARK options
1 parent c55b8c9 commit ae70b16

File tree

4 files changed

+224
-98
lines changed

4 files changed

+224
-98
lines changed

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

Lines changed: 20 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -6,9 +6,12 @@ import { SymbolKind, commands } from 'vscode';
66
import { Disposable } from 'vscode-jsonrpc';
77
import { ExecuteCommandRequest } from 'vscode-languageclient';
88
import { ALSSourceDirDescription, ExtensionState } from './ExtensionState';
9+
import { startVisualize } from './alsVisualizer';
910
import { AdaConfig, getOrAskForProgram, initializeConfig } from './debugConfigProvider';
1011
import { adaExtState, logger, mainOutputChannel } from './extension';
12+
import { loadGnatCoverageReport } from './gnattest';
1113
import { findAdaMain, getProjectFileRelPath, getSymbols } from './helpers';
14+
import { askSPARKOptions } from './sparkOptionsPicker';
1215
import {
1316
DEFAULT_PROBLEM_MATCHERS,
1417
SimpleTaskDef,
@@ -18,19 +21,17 @@ import {
1821
TASK_PROVE_SUPB_PLAIN_NAME,
1922
TASK_TYPE_SPARK,
2023
findBuildAndRunTask,
21-
getTasksWithPrefix,
22-
getConventionalTaskLabel,
23-
isFromWorkspace,
24-
workspaceTasksFirst,
2524
getBuildAndRunTaskName,
26-
getRunGNATemulatorTaskName,
2725
getBuildTaskName,
26+
getConventionalTaskLabel,
27+
getRunGNATemulatorTaskName,
28+
getTasksWithPrefix,
29+
isFromWorkspace,
2830
runTaskAndGetResult,
31+
workspaceTasksFirst,
2932
} from './taskProviders';
30-
import { createHelloWorldProject, walkthroughStartDebugging } from './walkthrough';
31-
import { loadGnatCoverageReport } from './gnattest';
32-
import { startVisualize } from './alsVisualizer';
3333
import { Hierarchy } from './visualizerTypes';
34+
import { createHelloWorldProject, walkthroughStartDebugging } from './walkthrough';
3435

3536
/**
3637
* Identifier for a hidden command used for building and running a project main.
@@ -1051,11 +1052,16 @@ async function sparkProveSubprogram(
10511052
uri: vscode.Uri,
10521053
range: vscode.Range,
10531054
): Promise<vscode.TaskExecution> {
1055+
const [tasks, cliArgs] = await Promise.all([
1056+
vscode.tasks.fetchTasks({ type: TASK_TYPE_SPARK }),
1057+
askSPARKOptions(),
1058+
]);
1059+
10541060
/**
10551061
* Get the 'Prove subprogram' task. Prioritize workspace tasks so that User
10561062
* customization of the task takes precedence.
10571063
*/
1058-
const task = (await vscode.tasks.fetchTasks({ type: TASK_TYPE_SPARK }))
1064+
const task = tasks
10591065
.sort(workspaceTasksFirst)
10601066
.find(
10611067
(t) =>
@@ -1098,6 +1104,11 @@ async function sparkProveSubprogram(
10981104
* with the same name in the task history.
10991105
*/
11001106
newTask.name = `${task.name} - ${fileBasename}:${range.start.line + 1}`;
1107+
1108+
/**
1109+
* Add the options chosen by the User
1110+
*/
1111+
taskDef.args.splice(regionArgIdx + 1, 0, ...cliArgs);
11011112
} else {
11021113
throw Error(
11031114
`Task '${getConventionalTaskLabel(task)}' is missing a '${regionArg}' argument`,

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

Lines changed: 113 additions & 78 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,8 @@
1+
/* eslint-disable @typescript-eslint/no-unsafe-return */
2+
/* eslint-disable @typescript-eslint/no-explicit-any */
3+
/* eslint-disable @typescript-eslint/no-unsafe-argument */
4+
/* eslint-disable @typescript-eslint/prefer-promise-reject-errors */
5+
/* eslint-disable @typescript-eslint/only-throw-error */
16
/*---------------------------------------------------------------------------------------------
27
* Copyright (c) Microsoft Corporation. All rights reserved.
38
* Licensed under the MIT License. See License.txt in the project root for license information.
@@ -9,22 +14,19 @@
914
*/
1015

1116
import {
12-
QuickPickItem,
13-
window,
1417
Disposable,
15-
CancellationToken,
16-
QuickInputButton,
1718
QuickInput,
18-
ExtensionContext,
19+
QuickInputButton,
1920
QuickInputButtons,
20-
Uri,
21+
QuickPickItem,
22+
window,
2123
} from 'vscode';
2224

2325
// -------------------------------------------------------
2426
// Helper code that wraps the API for the multi-step case.
2527
// -------------------------------------------------------
2628

27-
class InputFlowAction {
29+
export class InputFlowAction {
2830
static back = new InputFlowAction();
2931
static cancel = new InputFlowAction();
3032
static resume = new InputFlowAction();
@@ -37,11 +39,13 @@ interface QuickPickParameters<T extends QuickPickItem> {
3739
step: number;
3840
totalSteps: number;
3941
items: T[];
40-
activeItem?: T;
42+
canSelectMany?: boolean;
43+
activeItems?: T | T[];
44+
selectedItems?: T | T[];
4145
ignoreFocusOut?: boolean;
4246
placeholder: string;
4347
buttons?: QuickInputButton[];
44-
shouldResume: () => Thenable<boolean>;
48+
shouldResume?: () => Thenable<boolean>;
4549
}
4650

4751
interface InputBoxParameters {
@@ -50,47 +54,51 @@ interface InputBoxParameters {
5054
totalSteps: number;
5155
value: string;
5256
prompt: string;
53-
validate: (value: string) => Promise<string | undefined>;
57+
validate: (value: string) => string | undefined | Promise<string | undefined>;
5458
buttons?: QuickInputButton[];
5559
ignoreFocusOut?: boolean;
5660
placeholder?: string;
57-
shouldResume: () => Thenable<boolean>;
61+
shouldResume?: () => Thenable<boolean>;
5862
}
5963

60-
class MultiStepInput {
61-
static async run<T>(start: InputStep) {
64+
export class MultiStepInput {
65+
static async run(start: InputStep) {
6266
const input = new MultiStepInput();
6367
return input.stepThrough(start);
6468
}
6569

6670
private current?: QuickInput;
6771
private steps: InputStep[] = [];
6872

69-
private async stepThrough<T>(start: InputStep) {
70-
let step: InputStep | void = start;
71-
while (step) {
72-
this.steps.push(step);
73-
if (this.current) {
74-
this.current.enabled = false;
75-
this.current.busy = true;
76-
}
77-
try {
78-
step = await step(this);
79-
} catch (err) {
80-
if (err === InputFlowAction.back) {
81-
this.steps.pop();
82-
step = this.steps.pop();
83-
} else if (err === InputFlowAction.resume) {
84-
step = this.steps.pop();
85-
} else if (err === InputFlowAction.cancel) {
86-
step = undefined;
87-
} else {
88-
throw err;
73+
private async stepThrough(start: InputStep) {
74+
try {
75+
let step: InputStep | void = start;
76+
while (step) {
77+
this.steps.push(step);
78+
if (this.current) {
79+
this.current.enabled = false;
80+
this.current.busy = true;
81+
}
82+
try {
83+
step = await step(this);
84+
} catch (err) {
85+
if (err === InputFlowAction.back) {
86+
this.steps.pop();
87+
step = this.steps.pop();
88+
} else if (err === InputFlowAction.resume) {
89+
step = this.steps.pop();
90+
} else if (err === InputFlowAction.cancel) {
91+
step = undefined;
92+
throw err;
93+
} else {
94+
throw err;
95+
}
8996
}
9097
}
91-
}
92-
if (this.current) {
93-
this.current.dispose();
98+
} finally {
99+
if (this.current) {
100+
this.current.dispose();
101+
}
94102
}
95103
}
96104

@@ -99,56 +107,83 @@ class MultiStepInput {
99107
step,
100108
totalSteps,
101109
items,
102-
activeItem,
110+
canSelectMany,
111+
activeItems,
112+
selectedItems,
103113
ignoreFocusOut,
104114
placeholder,
105115
buttons,
106116
shouldResume,
107-
}: P) {
117+
}: P): Promise<
118+
| (P extends { canSelectMany: boolean } ? T[] : T)
119+
| (P extends { buttons: (infer I)[] } ? I : never)
120+
> {
108121
const disposables: Disposable[] = [];
109122
try {
110-
return await new Promise<T | (P extends { buttons: (infer I)[] } ? I : never)>(
111-
(resolve, reject) => {
112-
const input = window.createQuickPick<T>();
113-
input.title = title;
114-
input.step = step;
115-
input.totalSteps = totalSteps;
116-
input.ignoreFocusOut = ignoreFocusOut ?? false;
117-
input.placeholder = placeholder;
118-
input.items = items;
119-
if (activeItem) {
120-
input.activeItems = [activeItem];
123+
return await new Promise<
124+
| (P extends { canSelectMany: boolean } ? T[] : T)
125+
| (P extends { buttons: (infer I)[] } ? I : never)
126+
>((resolve, reject) => {
127+
const input = window.createQuickPick<T>();
128+
input.title = title;
129+
input.step = step;
130+
input.totalSteps = totalSteps;
131+
input.ignoreFocusOut = ignoreFocusOut ?? false;
132+
input.placeholder = placeholder;
133+
input.items = items;
134+
input.canSelectMany = canSelectMany ?? false;
135+
if (activeItems) {
136+
if (activeItems instanceof Array) {
137+
input.activeItems = activeItems;
138+
} else {
139+
input.activeItems = [activeItems];
121140
}
122-
input.buttons = [
123-
...(this.steps.length > 1 ? [QuickInputButtons.Back] : []),
124-
...(buttons || []),
125-
];
126-
disposables.push(
127-
input.onDidTriggerButton((item) => {
128-
if (item === QuickInputButtons.Back) {
129-
reject(InputFlowAction.back);
130-
} else {
131-
resolve(<any>item);
132-
}
133-
}),
134-
input.onDidChangeSelection((items) => resolve(items[0])),
135-
input.onDidHide(() => {
136-
(async () => {
137-
reject(
138-
shouldResume && (await shouldResume())
139-
? InputFlowAction.resume
140-
: InputFlowAction.cancel,
141-
);
142-
})().catch(reject);
143-
}),
144-
);
145-
if (this.current) {
146-
this.current.dispose();
141+
}
142+
if (selectedItems) {
143+
if (selectedItems instanceof Array) {
144+
input.selectedItems = selectedItems;
145+
} else {
146+
input.selectedItems = [selectedItems];
147147
}
148-
this.current = input;
149-
this.current.show();
150-
},
151-
);
148+
}
149+
input.buttons = [
150+
...(this.steps.length > 1 ? [QuickInputButtons.Back] : []),
151+
...(buttons || []),
152+
];
153+
disposables.push(
154+
input.onDidTriggerButton((item) => {
155+
if (item === QuickInputButtons.Back) {
156+
reject(InputFlowAction.back);
157+
} else {
158+
resolve(<any>item);
159+
}
160+
}),
161+
input.onDidChangeSelection((items) => {
162+
if (!canSelectMany) {
163+
resolve(<any>items[0]);
164+
}
165+
}),
166+
input.onDidAccept(() => {
167+
if (canSelectMany) {
168+
resolve(<any>input.selectedItems.concat());
169+
}
170+
}),
171+
input.onDidHide(() => {
172+
(async () => {
173+
reject(
174+
shouldResume && (await shouldResume())
175+
? InputFlowAction.resume
176+
: InputFlowAction.cancel,
177+
);
178+
})().catch(reject);
179+
}),
180+
);
181+
if (this.current) {
182+
this.current.dispose();
183+
}
184+
this.current = input;
185+
this.current.show();
186+
});
152187
} finally {
153188
disposables.forEach((d) => d.dispose());
154189
}

0 commit comments

Comments
 (0)