feat: replace stale dep notifs with "restart file" infoview button (#419

)

lean4-infoview-api/package.json

@@ -1,6 +1,6 @@
 {
   "name": "@leanprover/infoview-api",
-  "version": "0.2.1",
+  "version": "0.3.0",
   "description": "Types and API for @leanprover/infoview.",
   "scripts": {
     "watch": "tsc --watch",

lean4-infoview-api/src/infoviewApi.ts

@@ -57,6 +57,9 @@ export interface EditorApi {
   /** Highlight a range in a document in the editor. */
   showDocument(show: ShowDocumentParams): Promise<void>;
 
+  /** Restarts the given file. */
+  restartFile(uri: string): Promise<void>
+
   /**
    * Creates an RPC session for the given uri and returns the session id.
    * The extension takes care of keeping the RPC session alive.

lean4-infoview/package.json

@@ -1,6 +1,6 @@
 {
   "name": "@leanprover/infoview",
-  "version": "0.4.5",
+  "version": "0.5.0",
   "description": "An interactive display for the Lean 4 theorem prover.",
   "scripts": {
     "watch": "rollup --config --environment NODE_ENV:development --watch",
@@ -47,8 +47,9 @@
     "typescript": "^4.9.5"
   },
   "dependencies": {
-    "@leanprover/infoview-api": "~0.2.1",
+    "@leanprover/infoview-api": "~0.3.0",
     "@vscode/codicons": "^0.0.32",
+    "@vscode/webview-ui-toolkit": "^1.4.0",
     "es-module-shims": "^1.7.3",
     "marked": "^4.3.0",
     "react-fast-compare": "^3.2.2",

lean4-infoview/src/infoview/index.css

@@ -108,6 +108,13 @@ html,body {
 
 /* Headers for infoview */
 
+.restart-file-button {
+    position: fixed;
+    bottom: 10px;
+    right: 10px;
+    z-index: 37;
+}
+
 select {
     background-color: var(--vscode-dropdown-background);
     color: var(--vscode-dropdown-foreground);

lean4-infoview/src/infoview/info.tsx

@@ -300,9 +300,11 @@ function InfoAux(props: InfoProps) {
         // While `lake print-paths` is running, the output of Lake is shown as
         // info diagnostics on line 1.  However, all RPC requests block until
         // Lake is finished, so we don't see these diagnostics while Lake is
-        // building.  Therefore we show the LSP diagnostics on line 1 if the
+        // building. Therefore we show the LSP diagnostics on line 1 if the
         // server does not respond within half a second.
-        if (pos.line === 0 && lspDiagsHere.length) {
+        // The same is true for fatal header diagnostics like the stale dependency notification.
+        const isAllHeaderDiags = lspDiagsHere.length > 0 && lspDiagsHere.every(diag => diag.range.start.line === 0)
+        if (isAllHeaderDiags) {
             setTimeout(() => resolve({
                 pos,
                 status: 'updating',

lean4-infoview/src/infoview/main.tsx

@@ -1,6 +1,7 @@
 import * as React from 'react';
 import * as ReactDOM from 'react-dom/client';
 import type { DidCloseTextDocumentParams, Location, DocumentUri } from 'vscode-languageserver-protocol';
+import { VSCodeButton } from '@vscode/webview-ui-toolkit/react'
 
 import 'tachyons/css/tachyons.css';
 import '@vscode/codicons/dist/codicon.ttf';
@@ -65,6 +66,13 @@ function Main(props: {}) {
             {curUri && <div className="mv2">
                 <AllMessages uri={curUri} />
             </div>}
+            {curUri &&
+                <VSCodeButton
+                    className='restart-file-button'
+                    onClick={_ => ec.api.restartFile(curUri)}
+                    title='Restarts this file, rebuilding all of its outdated dependencies.'>
+                    Restart File
+                </VSCodeButton>}
         </div>
     }
 

vscode-lean4/package.json

@@ -894,8 +894,8 @@
 		"test": "node ./out/test/suite/runTest.js"
 	},
 	"dependencies": {
-		"@leanprover/infoview": "~0.4.5",
-		"@leanprover/infoview-api": "~0.2.1",
+		"@leanprover/infoview": "~0.5.0",
+		"@leanprover/infoview-api": "~0.3.0",
 		"axios": "^1.6.7",
 		"cheerio": "^1.0.0-rc.12",
 		"mobx": "^5.15.7",

vscode-lean4/src/infoview.ts

@@ -230,6 +230,20 @@ export class InfoProvider implements Disposable {
                 p2cConverter.asRange(show.selection)
             );
         },
+        restartFile: async (uri) => {
+            const client = this.clientProvider.findClient(uri)
+            if (!client) {
+                return
+            }
+
+            const path = Uri.parse(uri).fsPath
+            const document = workspace.textDocuments.find(doc => doc.uri.fsPath === path)
+            if (!document || document.isClosed) {
+                return
+            }
+
+            await client.restartFile(document)
+        },
 
         createRpcSession: async uri => {
             const client = this.clientProvider.findClient(uri);