Skip to content

Commit 9319114

Browse files
K-dizzledK-dizzled
committed
Create permanent status bar button
1 parent 5baf1f8 commit 9319114

14 files changed

+177
-64
lines changed

‎.prettierrc.json

+2-1
Original file line numberDiff line numberDiff line change
@@ -7,5 +7,6 @@
77
"printWidth": 80,
88
"importOrder": ["^[./]*llm/(.*)$", "^[./]*coqLsp/(.*)$", "^[./]*core/(.*)$", "^../", "^./"],
99
"importOrderSeparation": true,
10-
"importOrderSortSpecifiers": true
10+
"importOrderSortSpecifiers": true,
11+
"importOrderParserPlugins": ["typescript", "@trivago/prettier-plugin-sort-imports", "decorators-legacy"]
1112
}

‎package.json

+1-1
Original file line numberDiff line numberDiff line change
@@ -392,7 +392,7 @@
392392
"pretest": "npm run compile && npm run lint",
393393
"test": "npm run test-only",
394394
"clean": "rm -rf out",
395-
"rebuild": "npm run clean && npm run compile",
395+
"rebuild": "npm run clean && npm run compile && npm run format",
396396
"rebuild-test-resources": "cd ./src/test/resources/coqProj && make clean && make",
397397
"preclean-test": "npm run clean && npm run rebuild-test-resources && npm run compile && npm run lint",
398398
"clean-test": "npm run test-only",

‎src/coqLsp/coqLspClient.ts

+1-1
Original file line numberDiff line numberDiff line change
@@ -20,6 +20,7 @@ import {
2020
} from "vscode-languageclient";
2121

2222
import { EventLogger } from "../logging/eventLogger";
23+
import { logExecutionTime } from "../logging/timeMeasureDecorator";
2324
import { Uri } from "../utils/uri";
2425

2526
import { CoqLspClientConfig, CoqLspServerConfig } from "./coqLspConfig";
@@ -34,7 +35,6 @@ import {
3435
GoalRequest,
3536
PpString,
3637
} from "./coqLspTypes";
37-
import { logExecutionTime } from "../logging/timeMeasureDecorator";
3838

3939
export interface CoqLspClientInterface extends Disposable {
4040
getGoalsAtPoint(

‎src/coqParser/parseCoqFile.ts

+15-8
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,5 @@
11
import { readFileSync } from "fs";
2+
import { Result } from "ts-results";
23
import { Position, Range } from "vscode-languageclient";
34

45
import { CoqLspClientInterface } from "../coqLsp/coqLspClient";
@@ -13,11 +14,10 @@ import {
1314
import { Uri } from "../utils/uri";
1415

1516
import { ProofStep, Theorem, TheoremProof, Vernacexpr } from "./parsedTypes";
16-
import { Result } from "ts-results";
1717

1818
/**
19-
* TODO: [LspCoreRefactor] Refactor retrieveInitialGoal param
20-
* to be something more reasonable and readable.
19+
* TODO: [LspCoreRefactor] Refactor retrieveInitialGoal param
20+
* to be something more reasonable and readable.
2121
*/
2222
export async function parseCoqFile(
2323
uri: Uri,
@@ -30,7 +30,13 @@ export async function parseCoqFile(
3030
const documentText = readFileSync(uri.fsPath)
3131
.toString()
3232
.split("\n");
33-
return parseFlecheDocument(doc, documentText, client, uri, retrieveInitialGoal);
33+
return parseFlecheDocument(
34+
doc,
35+
documentText,
36+
client,
37+
uri,
38+
retrieveInitialGoal
39+
);
3440
})
3541
.catch((error) => {
3642
throw new CoqParsingError(
@@ -100,10 +106,11 @@ async function parseFlecheDocument(
100106
)
101107
);
102108
} else {
103-
// TODO: [LspCoreRefactor] Discuss invariants on initial_goal
104-
// and allow it's absence. As calculation of initial_goal
105-
// brings overhead of 100ms per theorem.
106-
let initialGoal: Result<Goal<PpString>[], Error> | null = null;
109+
// TODO: [LspCoreRefactor] Discuss invariants on initial_goal
110+
// and allow it's absence. As calculation of initial_goal
111+
// brings overhead of 100ms per theorem.
112+
let initialGoal: Result<Goal<PpString>[], Error> | null =
113+
null;
107114
if (retrieveInitialGoal) {
108115
initialGoal = await client.getGoalsAtPoint(
109116
doc.spans[i + 1].range.start,

‎src/core/contextTheoremRanker/euclidContextTheoremRanker.ts

+1-1
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,7 @@ import { goalAsTheoremString } from "./tokenUtils";
1212
*/
1313
export class EuclidContextTheoremsRanker implements ContextTheoremsRanker {
1414
public readonly needsUnwrappedNotations = true;
15-
15+
1616
rankContextTheorems(
1717
theorems: Theorem[],
1818
completionContext: CompletionContext

‎src/core/contextTheoremRanker/jaccardIndexContextTheoremsRanker.ts

+1-1
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,7 @@ export class JaccardIndexContextTheoremsRanker
1515
implements ContextTheoremsRanker
1616
{
1717
public readonly needsUnwrappedNotations = true;
18-
18+
1919
rankContextTheorems(
2020
theorems: Theorem[],
2121
completionContext: CompletionContext

‎src/core/contextTheoremRanker/weightedJaccardIndexTheoremRanker.ts

+1-1
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,7 @@ export class WeightedJaccardIndexContextTheoremsRanker
1515
implements ContextTheoremsRanker
1616
{
1717
public readonly needsUnwrappedNotations = true;
18-
18+
1919
rankContextTheorems(
2020
theorems: Theorem[],
2121
completionContext: CompletionContext

‎src/core/contextTheoremRanker/сosineContextTheoremRanker.ts

+1-1
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,7 @@ import { goalAsTheoremString } from "./tokenUtils";
1313
*/
1414
export class CosineContextTheoremsRanker implements ContextTheoremsRanker {
1515
public readonly needsUnwrappedNotations = true;
16-
16+
1717
rankContextTheorems(
1818
theorems: Theorem[],
1919
completionContext: CompletionContext

‎src/core/inspectSourceFile.ts

+6-2
Original file line numberDiff line numberDiff line change
@@ -18,7 +18,7 @@ export async function inspectSourceFile(
1818
fileVersion: number,
1919
shouldCompleteHole: (hole: ProofStep) => boolean,
2020
fileUri: Uri,
21-
client: CoqLspClientInterface,
21+
client: CoqLspClientInterface,
2222
rankerNeedsInitialGoals: boolean = true
2323
): Promise<AnalyzedFile> {
2424
const sourceFileEnvironment = await createSourceFileEnvironment(
@@ -84,7 +84,11 @@ export async function createSourceFileEnvironment(
8484
client: CoqLspClientInterface,
8585
rankerNeedsInitialGoals: boolean = true
8686
): Promise<SourceFileEnvironment> {
87-
const fileTheorems = await parseCoqFile(fileUri, client, rankerNeedsInitialGoals);
87+
const fileTheorems = await parseCoqFile(
88+
fileUri,
89+
client,
90+
rankerNeedsInitialGoals
91+
);
8892
const fileText = readFileSync(fileUri.fsPath);
8993
const dirPath = getSourceFolderPath(fileUri);
9094
if (!dirPath) {

‎src/extension/coqPilot.ts

+44-41
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,7 @@
11
import {
2-
ExtensionContext,
3-
ProgressLocation,
2+
ExtensionContext, // ProgressLocation,
43
TextEditor,
5-
commands,
6-
window,
4+
commands, // window,
75
workspace,
86
} from "vscode";
97

@@ -24,6 +22,7 @@ import { CoqProofChecker } from "../core/coqProofChecker";
2422
import { inspectSourceFile } from "../core/inspectSourceFile";
2523

2624
import { ProofStep } from "../coqParser/parsedTypes";
25+
import { logExecutionTime } from "../logging/timeMeasureDecorator";
2726
import { buildErrorCompleteLog } from "../utils/errorsUtils";
2827
import { Uri } from "../utils/uri";
2928

@@ -49,24 +48,24 @@ import {
4948
toVSCodeRange,
5049
} from "./positionRangeUtils";
5150
import { SettingsValidationError } from "./settingsValidationError";
52-
import { logExecutionTime } from "../logging/timeMeasureDecorator";
51+
import { StatusBarButton } from "./statusBarButton";
5352

5453
export const pluginId = "coqpilot";
5554
export const pluginName = "CoqPilot";
5655

5756
export class CoqPilot {
5857
private readonly globalExtensionState: GlobalExtensionState;
5958
private readonly vscodeExtensionContext: ExtensionContext;
59+
private subscriptions: { dispose(): any }[] = [];
6060

6161
private constructor(
6262
vscodeExtensionContext: ExtensionContext,
63-
globalExtensionState: GlobalExtensionState
63+
globalExtensionState: GlobalExtensionState,
64+
private readonly statusBarButton: StatusBarButton
6465
) {
6566
this.vscodeExtensionContext = vscodeExtensionContext;
6667
this.globalExtensionState = globalExtensionState;
6768

68-
console.log("CoqPilot extension is now active!");
69-
7069
this.registerEditorCommand(
7170
"perform_completion_under_cursor",
7271
this.performCompletionUnderCursor.bind(this)
@@ -83,9 +82,16 @@ export class CoqPilot {
8382
this.vscodeExtensionContext.subscriptions.push(this);
8483
}
8584

86-
static async create(vscodeExtensionContext: ExtensionContext) {
85+
static async create(
86+
vscodeExtensionContext: ExtensionContext,
87+
statusBarItem: StatusBarButton
88+
) {
8789
const globalExtensionState = await GlobalExtensionState.create();
88-
return new CoqPilot(vscodeExtensionContext, globalExtensionState);
90+
return new CoqPilot(
91+
vscodeExtensionContext,
92+
globalExtensionState,
93+
statusBarItem
94+
);
8995
}
9096

9197
async performCompletionUnderCursor(editor: TextEditor) {
@@ -112,38 +118,31 @@ export class CoqPilot {
112118
shouldCompleteHole: (hole: ProofStep) => boolean,
113119
editor: TextEditor
114120
) {
115-
await window.withProgress(
116-
{
117-
location: ProgressLocation.Window,
118-
title: `${pluginName}: In progress`,
119-
},
120-
async () => {
121-
try {
122-
await this.performSpecificCompletions(
123-
shouldCompleteHole,
124-
editor
125-
);
126-
} catch (e) {
127-
if (e instanceof SettingsValidationError) {
128-
e.showAsMessageToUser();
129-
} else if (e instanceof CoqLspStartupError) {
130-
showMessageToUserWithSettingsHint(
131-
EditorMessages.coqLspStartupFailure(e.path),
132-
"error",
133-
`${pluginId}.coqLspServerPath`
134-
);
135-
} else {
136-
showMessageToUser(
137-
e instanceof Error
138-
? EditorMessages.errorOccurred(e.message)
139-
: EditorMessages.objectWasThrownAsError(e),
140-
"error"
141-
);
142-
console.error(buildErrorCompleteLog(e));
143-
}
144-
}
121+
try {
122+
this.statusBarButton.showSpinner();
123+
124+
await this.performSpecificCompletions(shouldCompleteHole, editor);
125+
} catch (e) {
126+
if (e instanceof SettingsValidationError) {
127+
e.showAsMessageToUser();
128+
} else if (e instanceof CoqLspStartupError) {
129+
showMessageToUserWithSettingsHint(
130+
EditorMessages.coqLspStartupFailure(e.path),
131+
"error",
132+
`${pluginId}.coqLspServerPath`
133+
);
134+
} else {
135+
showMessageToUser(
136+
e instanceof Error
137+
? EditorMessages.errorOccurred(e.message)
138+
: EditorMessages.objectWasThrownAsError(e),
139+
"error"
140+
);
141+
console.error(buildErrorCompleteLog(e));
145142
}
146-
);
143+
} finally {
144+
this.statusBarButton.hideSpinner();
145+
}
147146
}
148147

149148
private async performSpecificCompletions(
@@ -327,9 +326,13 @@ export class CoqPilot {
327326
fn
328327
);
329328
this.vscodeExtensionContext.subscriptions.push(disposable);
329+
this.subscriptions.push(disposable);
330330
}
331331

332332
dispose(): void {
333+
// This is not the same as vscodeExtensionContext.subscriptions
334+
// As it doesn't contain the statusBar item and the toggle command
335+
this.subscriptions.forEach((d) => d.dispose());
333336
this.globalExtensionState.dispose();
334337
}
335338
}

‎src/extension/globalExtensionState.ts

+1-1
Original file line numberDiff line numberDiff line change
@@ -95,9 +95,9 @@ export class GlobalExtensionState {
9595
}
9696

9797
dispose(): void {
98+
this.coqLspClient.dispose();
9899
disposeServices(this.llmServices);
99100
this.logWriter.dispose();
100-
this.coqLspClient.dispose();
101101
fs.rmSync(this.llmServicesLogsDir, { recursive: true, force: true });
102102
this.logOutputChannel.dispose();
103103
}

‎src/extension/statusBarButton.ts

+74
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,74 @@
1+
import {
2+
ExtensionContext,
3+
StatusBarAlignment,
4+
StatusBarItem,
5+
commands,
6+
window,
7+
} from "vscode";
8+
9+
import { pluginId, pluginName } from "./coqPilot";
10+
11+
export class StatusBarButton {
12+
private statusBarItem: StatusBarItem;
13+
private isActive: boolean;
14+
private context: ExtensionContext;
15+
private toggleCallback: (
16+
isActive: boolean,
17+
context: ExtensionContext
18+
) => void;
19+
20+
constructor(
21+
context: ExtensionContext,
22+
toggleCallback: (isActive: boolean, context: ExtensionContext) => void
23+
) {
24+
this.context = context;
25+
this.isActive = false;
26+
this.toggleCallback = toggleCallback;
27+
28+
this.statusBarItem = window.createStatusBarItem(
29+
StatusBarAlignment.Left,
30+
0
31+
);
32+
this.updateStatusBar();
33+
34+
this.statusBarItem.show();
35+
this.context.subscriptions.push(this.statusBarItem);
36+
37+
const command = `${pluginId}.toggleExtension`;
38+
this.statusBarItem.command = command;
39+
const toggleCommand = commands.registerCommand(
40+
command,
41+
this.toggle.bind(this)
42+
);
43+
this.context.subscriptions.push(toggleCommand);
44+
}
45+
46+
toggle() {
47+
this.isActive = !this.isActive;
48+
this.updateStatusBar();
49+
this.toggleCallback(this.isActive, this.context);
50+
}
51+
52+
private updateStatusBar() {
53+
if (this.isActive) {
54+
this.statusBarItem.text = `$(debug-stop) ${pluginName}: Running`;
55+
this.statusBarItem.tooltip = "Click to stop the extension";
56+
} else {
57+
this.statusBarItem.text = `$(debug-stop) ${pluginName}: Stopped`;
58+
this.statusBarItem.tooltip = "Click to start the extension";
59+
}
60+
}
61+
62+
public showSpinner() {
63+
this.statusBarItem.text = `$(sync~spin) ${pluginName}: In progress`;
64+
this.statusBarItem.tooltip = "Operation in progress...";
65+
}
66+
67+
public hideSpinner() {
68+
this.updateStatusBar();
69+
}
70+
71+
public dispose() {
72+
this.statusBarItem.dispose();
73+
}
74+
}

‎src/logging/timeMeasureDecorator.ts

+3-3
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
/**
2-
* A decorator that logs the execution time of a method.
2+
* A decorator that logs the execution time of a method.
33
* Execution time is logged into console in milliseconds.
4-
*
4+
*
55
* (Note: typescript supports decorators only for class methods).
66
*/
77
export function logExecutionTime(
@@ -42,4 +42,4 @@ export function logExecutionTime(
4242
};
4343

4444
return descriptor;
45-
}
45+
}

0 commit comments

Comments
 (0)