test: don't show modal dialogs in tests

leanprover · Oct 18, 2023 · 5cab99c · 5cab99c
1 parent e14d04b
commit 5cab99c
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 3 deletions.
diff --git a/vscode-lean4/src/utils/clientProvider.ts b/vscode-lean4/src/utils/clientProvider.ts
@@ -48,7 +48,7 @@ export class LeanClientProvider implements Disposable {
         this.subscriptions.push(
             commands.registerCommand('lean4.restartFile', () => this.restartFile()),
             commands.registerCommand('lean4.refreshFileDependencies', () => this.restartFile()),
-            commands.registerCommand('lean4.restartServer', () => this.restartActiveClient()),
+            commands.registerCommand('lean4.restartServer', showDialog => this.restartActiveClient(showDialog ?? true)),
             commands.registerCommand('lean4.stopServer', () => this.stopActiveClient())
         );
 
@@ -155,7 +155,12 @@ export class LeanClientProvider implements Disposable {
         }
     }
 
-    private async restartActiveClient() {
+    private async restartActiveClient(showDialog: boolean = true) {
+        if (!showDialog) {
+            void this.activeClient?.restart();
+            return
+        }
+
         const result: string | undefined = await window.showInformationMessage(
             'Restart Lean 4 server to re-elaborate all open files?',
             { modal: true },

diff --git a/vscode-lean4/test/suite/utils/helpers.ts b/vscode-lean4/test/suite/utils/helpers.ts
@@ -392,7 +392,7 @@ export async function restartLeanServer(client: LeanClient, retries=60, delay=10
     client.restarted(() => { stateChanges.push('restarted'); });
     client.serverFailed(() => { stateChanges.push('failed'); });
 
-    await vscode.commands.executeCommand('lean4.restartServer');
+    await vscode.commands.executeCommand('lean4.restartServer', false);
 
     while (count < retries){
         const index = stateChanges.indexOf('restarted');