feat: restart file button in 'fetch cache for focused file' command

leanprover · Oct 28, 2024 · a4eb1ce · a4eb1ce
1 parent 9ea8703
commit a4eb1ce
Show file tree

Hide file tree

Showing 3 changed files with 61 additions and 35 deletions.
diff --git a/vscode-lean4/src/leanclient.ts b/vscode-lean4/src/leanclient.ts
@@ -188,7 +188,7 @@ export class LeanClient implements Disposable {
         // Should only be called from `restart`
 
         const startTime = Date.now()
-        progress.report({ increment: 0 })
+        progress.report({})
         this.client = await this.setupClient()
 
         let insideRestart = true
@@ -215,7 +215,6 @@ export class LeanClient implements Disposable {
                     }
                 }
             })
-            progress.report({ increment: 80 })
             await this.client.start()
             const version = this.client.initializeResult?.serverInfo?.version
             if (version && new SemVer(version).compare('0.2.0') < 0) {
@@ -314,14 +313,16 @@ export class LeanClient implements Disposable {
             return 'IsRestarting'
         }
         this.isRestarting = true // Ensure that client cannot be restarted in the mean-time
+        try {
+            if (this.isStarted()) {
+                await this.stop()
+            }
 
-        if (this.isStarted()) {
-            await this.stop()
+            await action()
+        } finally {
+            this.isRestarting = false
         }
 
-        await action()
-
-        this.isRestarting = false
         await this.restart()
 
         return 'Success'

diff --git a/vscode-lean4/src/projectoperations.ts b/vscode-lean4/src/projectoperations.ts
@@ -7,7 +7,13 @@ import { LeanClientProvider } from './utils/clientProvider'
 import { toExtUri } from './utils/exturi'
 import { cacheNotFoundError, lake, LakeRunner } from './utils/lake'
 import { DirectGitDependency, Manifest, ManifestReadError, parseManifestInFolder } from './utils/manifest'
-import { displayError, displayInformation, displayInformationWithInput, displayWarningWithInput } from './utils/notifs'
+import {
+    displayError,
+    displayInformation,
+    displayInformationWithInput,
+    displayInformationWithOptionalInput,
+    displayWarningWithInput,
+} from './utils/notifs'
 
 type DependencyToolchainResult =
     | { kind: 'Success'; dependencyToolchain: string }
@@ -182,8 +188,10 @@ export class ProjectOperationProvider implements Disposable {
                 return
             }
 
-            displayInformation(
+            displayInformationWithOptionalInput(
                 `Mathlib build artifact cache for '${relativeActiveFileUri.fsPath}' fetched successfully.`,
+                'Restart File',
+                () => this.clientProvider.restartFile(activeFileUri),
             )
         })
     }
@@ -392,34 +400,32 @@ export class ProjectOperationProvider implements Disposable {
             return
         }
         this.isRunningOperation = true
+        try {
+            if (!this.clientProvider) {
+                displayError('Lean client has not loaded yet.')
+                return
+            }
 
-        if (!this.clientProvider) {
-            displayError('Lean client has not loaded yet.')
-            this.isRunningOperation = false
-            return
-        }
-
-        const activeClient: LeanClient | undefined = this.clientProvider.getActiveClient()
-        if (!activeClient) {
-            displayError('No active client.')
-            this.isRunningOperation = false
-            return
-        }
+            const activeClient: LeanClient | undefined = this.clientProvider.getActiveClient()
+            if (!activeClient) {
+                displayError('No active client.')
+                return
+            }
 
-        if (activeClient.folderUri.scheme === 'untitled') {
-            displayError('Cannot run project action for untitled files.')
-            this.isRunningOperation = false
-            return
-        }
+            if (activeClient.folderUri.scheme === 'untitled') {
+                displayError('Cannot run project action for untitled files.')
+                return
+            }
 
-        const lakeRunner: LakeRunner = lake(this.channel, activeClient.folderUri, context)
+            const lakeRunner: LakeRunner = lake(this.channel, activeClient.folderUri, context)
 
-        const result: 'Success' | 'IsRestarting' = await activeClient.withStoppedClient(() => command(lakeRunner))
-        if (result === 'IsRestarting') {
-            displayError('Cannot run project action while restarting the server.')
+            const result: 'Success' | 'IsRestarting' = await activeClient.withStoppedClient(() => command(lakeRunner))
+            if (result === 'IsRestarting') {
+                displayError('Cannot run project action while restarting the server.')
+            }
+        } finally {
+            this.isRunningOperation = false
         }
-
-        this.isRunningOperation = false
     }
 
     dispose() {

diff --git a/vscode-lean4/src/utils/clientProvider.ts b/vscode-lean4/src/utils/clientProvider.ts
@@ -1,4 +1,5 @@
 import { LeanFileProgressProcessingInfo, ServerStoppedReason } from '@leanprover/infoview-api'
+import path from 'path'
 import { Disposable, EventEmitter, OutputChannel, TextDocument, commands, window, workspace } from 'vscode'
 import {
     checkAll,
@@ -72,8 +73,8 @@ export class LeanClientProvider implements Disposable {
         )
 
         this.subscriptions.push(
-            commands.registerCommand('lean4.restartFile', () => this.restartFile()),
-            commands.registerCommand('lean4.refreshFileDependencies', () => this.restartFile()),
+            commands.registerCommand('lean4.restartFile', () => this.restartActiveFile()),
+            commands.registerCommand('lean4.refreshFileDependencies', () => this.restartActiveFile()),
             commands.registerCommand('lean4.restartServer', () => this.restartActiveClient()),
             commands.registerCommand('lean4.stopServer', () => this.stopActiveClient()),
         )
@@ -143,7 +144,25 @@ export class LeanClientProvider implements Disposable {
         this.processingInstallChanged = false
     }
 
-    private restartFile() {
+    restartFile(uri: ExtUri) {
+        const fileName = uri.scheme === 'file' ? path.basename(uri.fsPath) : 'untitled file'
+
+        const client: LeanClient | undefined = this.findClient(uri)
+        if (!client || !client.isRunning()) {
+            displayError(`No active client for '${fileName}'.`)
+            return
+        }
+
+        const doc = workspace.textDocuments.find(doc => uri.equalsUri(doc.uri))
+        if (!doc) {
+            displayError(`'${fileName}' was closed in the meantime.`)
+            return
+        }
+
+        void client.restartFile(doc)
+    }
+
+    restartActiveFile() {
         if (!this.activeClient || !this.activeClient.isRunning()) {
             displayError('No active client.')
             return