Skip to content

Commit 397db7f

Browse files
author
automatic-merge
committed
Merge remote branch 'origin/master' into edge
2 parents a18b5ee + 6b96842 commit 397db7f

File tree

4 files changed

+431
-21
lines changed

4 files changed

+431
-21
lines changed

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

Lines changed: 26 additions & 10 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.
@@ -87,6 +88,7 @@ export const CMD_GET_PROJECT_FILE = 'ada.getProjectFile';
8788
export const CMD_SPARK_LIMIT_SUBP_ARG = 'ada.spark.limitSubpArg';
8889
export const CMD_SPARK_LIMIT_REGION_ARG = 'ada.spark.limitRegionArg';
8990
export const CMD_SPARK_PROVE_SUBP = 'ada.spark.proveSubprogram';
91+
const CMD_SPARK_ASK_OPTIONS = 'ada.spark.askSPARKOptions';
9092

9193
/**
9294
* Identifier for the command that shows the extension's output in the Output panel.
@@ -246,6 +248,8 @@ export function registerCommands(context: vscode.ExtensionContext, clients: Exte
246248
vscode.commands.registerCommand(CMD_SPARK_PROVE_SUBP, sparkProveSubprogram),
247249
);
248250

251+
context.subscriptions.push(commands.registerCommand(CMD_SPARK_ASK_OPTIONS, askSPARKOptions));
252+
249253
context.subscriptions.push(
250254
commands.registerCommand('ada.loadGnatCovXMLReport', loadGnatCovXMLReport),
251255
);
@@ -1055,7 +1059,8 @@ async function sparkProveSubprogram(
10551059
* Get the 'Prove subprogram' task. Prioritize workspace tasks so that User
10561060
* customization of the task takes precedence.
10571061
*/
1058-
const task = (await vscode.tasks.fetchTasks({ type: TASK_TYPE_SPARK }))
1062+
const tasks = await vscode.tasks.fetchTasks({ type: TASK_TYPE_SPARK });
1063+
const task = tasks
10591064
.sort(workspaceTasksFirst)
10601065
.find(
10611066
(t) =>
@@ -1088,7 +1093,7 @@ async function sparkProveSubprogram(
10881093
*/
10891094
const taskDef = newTask.definition as SimpleTaskDef;
10901095
assert(taskDef.args);
1091-
const regionArg = '${command:ada.spark.limitSubpArg}';
1096+
const regionArg = `\${command:${CMD_SPARK_LIMIT_SUBP_ARG}}`;
10921097
const regionArgIdx = taskDef.args.findIndex((arg) => arg == regionArg);
10931098
if (regionArgIdx >= 0) {
10941099
const fileBasename = basename(uri.fsPath);
@@ -1098,6 +1103,17 @@ async function sparkProveSubprogram(
10981103
* with the same name in the task history.
10991104
*/
11001105
newTask.name = `${task.name} - ${fileBasename}:${range.start.line + 1}`;
1106+
1107+
/**
1108+
* Add a command to ask the User for options. We do this instead of
1109+
* pre-evaluating the options so that all invocations on the same
1110+
* subprogram have the same set of (unevaluated) arguments, which means
1111+
* that only one task shows up in the task history for each subprogram.
1112+
* If we pre-evaluated the options, then each different set of User
1113+
* choices would yield a different entry in the task history which is
1114+
* noisy.
1115+
*/
1116+
taskDef.args.splice(regionArgIdx + 1, 0, `\${command:${CMD_SPARK_ASK_OPTIONS}}`);
11011117
} else {
11021118
throw Error(
11031119
`Task '${getConventionalTaskLabel(task)}' is missing a '${regionArg}' argument`,

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

Lines changed: 268 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,268 @@
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 */
6+
/*---------------------------------------------------------------------------------------------
7+
* Copyright (c) Microsoft Corporation. All rights reserved.
8+
* Licensed under the MIT License. See License.txt in the project root for license information.
9+
*--------------------------------------------------------------------------------------------*/
10+
11+
/**
12+
* This file is largely based on the Quick Picker Sample project by Microsoft,
13+
* with some additions and fixes by AdaCore.
14+
*/
15+
16+
import {
17+
Disposable,
18+
QuickInput,
19+
QuickInputButton,
20+
QuickInputButtons,
21+
QuickPickItem,
22+
window,
23+
} from 'vscode';
24+
25+
// -------------------------------------------------------
26+
// Helper code that wraps the API for the multi-step case.
27+
// -------------------------------------------------------
28+
29+
export class InputFlowAction {
30+
static back = new InputFlowAction();
31+
static cancel = new InputFlowAction();
32+
static resume = new InputFlowAction();
33+
}
34+
35+
type InputStep = (input: MultiStepInput) => Thenable<InputStep | void>;
36+
37+
interface QuickPickParameters<T extends QuickPickItem> {
38+
title: string;
39+
step: number;
40+
totalSteps: number;
41+
items: T[];
42+
canSelectMany?: boolean;
43+
activeItems?: T | T[];
44+
selectedItems?: T | T[];
45+
ignoreFocusOut?: boolean;
46+
placeholder: string;
47+
buttons?: QuickInputButton[];
48+
shouldResume?: () => Thenable<boolean>;
49+
}
50+
51+
interface InputBoxParameters {
52+
title: string;
53+
step: number;
54+
totalSteps: number;
55+
value: string;
56+
prompt: string;
57+
validate: (value: string) => string | undefined | Promise<string | undefined>;
58+
buttons?: QuickInputButton[];
59+
ignoreFocusOut?: boolean;
60+
placeholder?: string;
61+
shouldResume?: () => Thenable<boolean>;
62+
}
63+
64+
export class MultiStepInput {
65+
static async run(start: InputStep) {
66+
const input = new MultiStepInput();
67+
return input.stepThrough(start);
68+
}
69+
70+
private current?: QuickInput;
71+
private steps: InputStep[] = [];
72+
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+
}
96+
}
97+
}
98+
} finally {
99+
if (this.current) {
100+
this.current.dispose();
101+
}
102+
}
103+
}
104+
105+
async showQuickPick<T extends QuickPickItem, P extends QuickPickParameters<T>>({
106+
title,
107+
step,
108+
totalSteps,
109+
items,
110+
canSelectMany,
111+
activeItems,
112+
selectedItems,
113+
ignoreFocusOut,
114+
placeholder,
115+
buttons,
116+
shouldResume,
117+
}: P): Promise<
118+
| (P extends { canSelectMany: boolean } ? T[] : T)
119+
| (P extends { buttons: (infer I)[] } ? I : never)
120+
> {
121+
const disposables: Disposable[] = [];
122+
try {
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];
140+
}
141+
}
142+
if (selectedItems) {
143+
if (selectedItems instanceof Array) {
144+
input.selectedItems = selectedItems;
145+
} else {
146+
input.selectedItems = [selectedItems];
147+
}
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+
});
187+
} finally {
188+
disposables.forEach((d) => d.dispose());
189+
}
190+
}
191+
192+
async showInputBox<P extends InputBoxParameters>({
193+
title,
194+
step,
195+
totalSteps,
196+
value,
197+
prompt,
198+
validate,
199+
buttons,
200+
ignoreFocusOut,
201+
placeholder,
202+
shouldResume,
203+
}: P) {
204+
const disposables: Disposable[] = [];
205+
try {
206+
return await new Promise<string | (P extends { buttons: (infer I)[] } ? I : never)>(
207+
(resolve, reject) => {
208+
const input = window.createInputBox();
209+
input.title = title;
210+
input.step = step;
211+
input.totalSteps = totalSteps;
212+
input.value = value || '';
213+
input.prompt = prompt;
214+
input.ignoreFocusOut = ignoreFocusOut ?? false;
215+
input.placeholder = placeholder;
216+
input.buttons = [
217+
...(this.steps.length > 1 ? [QuickInputButtons.Back] : []),
218+
...(buttons || []),
219+
];
220+
let validating = validate('');
221+
disposables.push(
222+
input.onDidTriggerButton((item) => {
223+
if (item === QuickInputButtons.Back) {
224+
reject(InputFlowAction.back);
225+
} else {
226+
resolve(<any>item);
227+
}
228+
}),
229+
input.onDidAccept(async () => {
230+
const value = input.value;
231+
input.enabled = false;
232+
input.busy = true;
233+
if (!(await validate(value))) {
234+
resolve(value);
235+
}
236+
input.enabled = true;
237+
input.busy = false;
238+
}),
239+
input.onDidChangeValue(async (text) => {
240+
const current = validate(text);
241+
validating = current;
242+
const validationMessage = await current;
243+
if (current === validating) {
244+
input.validationMessage = validationMessage;
245+
}
246+
}),
247+
input.onDidHide(() => {
248+
(async () => {
249+
reject(
250+
shouldResume && (await shouldResume())
251+
? InputFlowAction.resume
252+
: InputFlowAction.cancel,
253+
);
254+
})().catch(reject);
255+
}),
256+
);
257+
if (this.current) {
258+
this.current.dispose();
259+
}
260+
this.current = input;
261+
this.current.show();
262+
},
263+
);
264+
} finally {
265+
disposables.forEach((d) => d.dispose());
266+
}
267+
}
268+
}

0 commit comments

Comments
 (0)