From 86291b4925844b523adcb0ee79f2397698c18a0b Mon Sep 17 00:00:00 2001
From: mhuisi <mhuisi@protonmail.com>
Date: Tue, 17 Oct 2023 10:54:47 +0200
Subject: [PATCH] feat: notification for imports-out-of-date error

---
 vscode-lean4/src/leanclient.ts | 37 +++++++++++++++++++++++++++++++++-
 1 file changed, 36 insertions(+), 1 deletion(-)

diff --git a/vscode-lean4/src/leanclient.ts b/vscode-lean4/src/leanclient.ts
index 162982004..c144481a5 100644
--- a/vscode-lean4/src/leanclient.ts
+++ b/vscode-lean4/src/leanclient.ts
@@ -1,8 +1,9 @@
 import { TextDocument, EventEmitter, Diagnostic,
     DocumentHighlight, Range, DocumentHighlightKind, workspace,
     Disposable, Uri, ConfigurationChangeEvent, OutputChannel, DiagnosticCollection,
-    WorkspaceFolder, window } from 'vscode'
+    WorkspaceFolder, window, commands } from 'vscode'
 import {
+    DiagnosticSeverity,
     DidChangeTextDocumentParams,
     DidCloseTextDocumentParams,
     DidOpenTextDocumentNotification,
@@ -30,6 +31,7 @@ import { logger } from './utils/logger'
 import { SemVer } from 'semver';
 import { fileExists, isFileInFolder } from './utils/fsHelper';
 import { c2pConverter, p2cConverter, patchConverters } from './utils/converters'
+import path = require('path')
 
 const escapeRegExp = (s: string) => s.replace(/[.*+?^${}()|[\]\\]/g, '\\$&');
 
@@ -98,6 +100,39 @@ export class LeanClient implements Disposable {
         this.elanDefaultToolchain = elanDefaultToolchain;
         if (!this.toolchainPath) this.toolchainPath = toolchainPath();
         this.subscriptions.push(workspace.onDidChangeConfiguration((e) => this.configChanged(e)));
+
+        this.subscriptions.push(this.diagnostics(params => this.checkForImportsOutdatedError(params)))
+    }
+
+    private async checkForImportsOutdatedError(params: PublishDiagnosticsParams) {
+        const fileUri = Uri.parse(params.uri)
+        const fileName = path.basename(fileUri.fsPath)
+        const isImportsOutdatedError = params.diagnostics.some(d =>
+            d.severity === DiagnosticSeverity.Error
+                && d.message.includes('Imports are out of date and must be rebuilt')
+                && d.range.start.line === 0
+                && d.range.start.character === 0
+                && d.range.end.line === 0
+                && d.range.end.character === 0)
+        if (!isImportsOutdatedError) {
+            return
+        }
+
+        const message = `Imports of '${fileName}' are out of date and must be rebuilt.`
+        const input = 'Rebuild Imports'
+        const choice = await window.showInformationMessage(message, input)
+        if (choice !== input) {
+            return
+        }
+
+        const fileUriString = fileUri.toString()
+        const document = workspace.textDocuments.find(doc => doc.uri.toString() === fileUriString)
+        if (!document || document.isClosed) {
+            void window.showErrorMessage(`'${fileName}' was closed in the meantime. Imports will not be rebuilt.`)
+            return
+        }
+
+        await this.restartFile(document)
     }
 
     dispose(): void {