From 5cab99c6471294e7ebeabe8977d74ef6e42d216a Mon Sep 17 00:00:00 2001
From: mhuisi <mhuisi@protonmail.com>
Date: Wed, 18 Oct 2023 19:21:25 +0200
Subject: [PATCH] test: don't show modal dialogs in tests

---
 vscode-lean4/src/utils/clientProvider.ts | 9 +++++++--
 vscode-lean4/test/suite/utils/helpers.ts | 2 +-
 2 files changed, 8 insertions(+), 3 deletions(-)

diff --git a/vscode-lean4/src/utils/clientProvider.ts b/vscode-lean4/src/utils/clientProvider.ts
index e24f81c14..f2d443e25 100644
--- 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
index 8197dbd02..4ee946f41 100644
--- 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');