refactor: use LeanEditorProvider everywhere

vscode-lean4/src/abbreviationview.ts

@@ -1,6 +1,7 @@
 import { AbbreviationProvider } from '@leanprover/unicode-input'
-import { Disposable, ViewColumn, WebviewPanel, commands, window } from 'vscode'
+import { Disposable, WebviewPanel, commands, window } from 'vscode'
 import { FileUri } from './utils/exturi'
+import { viewColumnOfInfoView } from './utils/viewColumn'
 
 function escapeHtml(s: string) {
     return s
@@ -29,7 +30,7 @@ export class AbbreviationView implements Disposable {
         this.webviewPanel = window.createWebviewPanel(
             'lean4_abbreviationview',
             'AbbreviationView',
-            { viewColumn: ViewColumn.Beside },
+            { viewColumn: viewColumnOfInfoView() },
             {
                 enableScripts: true,
                 enableFindWidget: true,

vscode-lean4/src/diagnostics/fullDiagnostics.ts

@@ -1,7 +1,8 @@
 import { SemVer } from 'semver'
-import { Disposable, OutputChannel, TextDocument, commands, env, window, workspace } from 'vscode'
+import { Disposable, OutputChannel, commands, env } from 'vscode'
 import { ExecutionExitCode, ExecutionResult } from '../utils/batch'
-import { ExtUri, FileUri, extUriEquals, toExtUri } from '../utils/exturi'
+import { FileUri } from '../utils/exturi'
+import { lean } from '../utils/leanEditorProvider'
 import { displayNotification, displayNotificationWithInput } from '../utils/notifs'
 import { findLeanProjectRoot } from '../utils/projectInfo'
 import {
@@ -134,46 +135,10 @@ export async function performFullDiagnosis(
 export class FullDiagnosticsProvider implements Disposable {
     private subscriptions: Disposable[] = []
     private outputChannel: OutputChannel
-    // Under normal circumstances, we would use the last active `LeanClient` from `LeanClientProvider.getActiveClient()`
-    // to determine the document that the user is currently working on.
-    // However, when providing setup diagnostics, there might not be an active client due to errors in the user's setup,
-    // in which case we still want to provide adequate diagnostics. Hence, we track the last active lean document
-    // separately, regardless of whether there is an actual `LeanClient` managing it.
-    private lastActiveLeanDocumentUri: ExtUri | undefined
 
     constructor(outputChannel: OutputChannel) {
         this.outputChannel = outputChannel
 
-        if (window.activeTextEditor !== undefined) {
-            this.lastActiveLeanDocumentUri = FullDiagnosticsProvider.getLean4DocUri(window.activeTextEditor.document)
-        }
-
-        window.onDidChangeActiveTextEditor(e => {
-            if (e === undefined) {
-                return
-            }
-            const docUri = FullDiagnosticsProvider.getLean4DocUri(e.document)
-            if (docUri === undefined) {
-                return
-            }
-
-            this.lastActiveLeanDocumentUri = docUri
-        }, this.subscriptions)
-        workspace.onDidCloseTextDocument(doc => {
-            if (this.lastActiveLeanDocumentUri === undefined) {
-                return
-            }
-
-            const docUri = FullDiagnosticsProvider.getLean4DocUri(doc)
-            if (docUri === undefined) {
-                return
-            }
-
-            if (extUriEquals(docUri, this.lastActiveLeanDocumentUri)) {
-                this.lastActiveLeanDocumentUri = undefined
-            }
-        }, this.subscriptions)
-
         this.subscriptions.push(
             commands.registerCommand('lean4.troubleshooting.showSetupInformation', () =>
                 this.performAndDisplayFullDiagnosis(),
@@ -182,14 +147,20 @@ export class FullDiagnosticsProvider implements Disposable {
     }
 
     async performAndDisplayFullDiagnosis() {
+        // Under normal circumstances, we would use the last active `LeanClient` from `LeanClientProvider.getActiveClient()`
+        // to determine the document that the user is currently working on.
+        // However, when providing setup diagnostics, there might not be an active client due to errors in the user's setup,
+        // in which case we still want to provide adequate diagnostics. Hence, we use the last active Lean document,
+        // regardless of whether there is an actual `LeanClient` managing it.
+        const lastActiveLeanDocumentUri = lean.lastActiveLeanDocument?.extUri
         const projectUri =
-            this.lastActiveLeanDocumentUri !== undefined && this.lastActiveLeanDocumentUri.scheme === 'file'
-                ? await findLeanProjectRoot(this.lastActiveLeanDocumentUri)
+            lastActiveLeanDocumentUri !== undefined && lastActiveLeanDocumentUri.scheme === 'file'
+                ? await findLeanProjectRoot(lastActiveLeanDocumentUri)
                 : undefined
         if (projectUri === 'FileNotFound') {
             displayNotification(
                 'Error',
-                `Cannot display setup information for file that does not exist in the file system: ${this.lastActiveLeanDocumentUri}. Please choose a different file to display the setup information for.`,
+                `Cannot display setup information for file that does not exist in the file system: ${lastActiveLeanDocumentUri}. Please choose a different file to display the setup information for.`,
             )
             return
         }
@@ -202,13 +173,6 @@ export class FullDiagnosticsProvider implements Disposable {
         }
     }
 
-    private static getLean4DocUri(doc: TextDocument): ExtUri | undefined {
-        if (doc.languageId !== 'lean4') {
-            return undefined
-        }
-        return toExtUri(doc.uri)
-    }
-
     dispose() {
         for (const s of this.subscriptions) {
             s.dispose()

vscode-lean4/src/extension.ts

@@ -20,9 +20,9 @@ import { LeanClientProvider } from './utils/clientProvider'
 import { LeanConfigWatchService } from './utils/configwatchservice'
 import { PATH, setProcessEnvPATH } from './utils/envPath'
 import { onEventWhile, withoutReentrancy } from './utils/events'
-import { FileUri, toExtUri } from './utils/exturi'
+import { FileUri } from './utils/exturi'
 import { displayInternalErrorsIn } from './utils/internalErrors'
-import { leanEditor, registerLeanEditor } from './utils/leanEditorProvider'
+import { lean, LeanEditor, registerLeanEditor } from './utils/leanEditorProvider'
 import { LeanInstaller } from './utils/leanInstaller'
 import { displayNotification, displayNotificationWithInput } from './utils/notifs'
 import { PathExtensionProvider } from './utils/pathExtensionProvider'
@@ -32,32 +32,29 @@ async function setLeanFeatureSetActive(isActive: boolean) {
     await commands.executeCommand('setContext', 'lean4.isLeanFeatureSetActive', isActive)
 }
 
-async function findLean4DocumentProjectUri(doc: TextDocument): Promise<FileUri | undefined | 'InvalidDocument'> {
-    const docUri = toExtUri(doc.uri)
-    if (docUri === undefined || doc.languageId !== 'lean4') {
-        return 'InvalidDocument'
-    }
+async function findLeanEditorProjectUri(editor: LeanEditor): Promise<FileUri | undefined | 'InvalidProject'> {
+    const docUri = editor.documentExtUri
     const projectUri = docUri.scheme === 'file' ? await findLeanProjectRoot(docUri) : undefined
     if (projectUri === 'FileNotFound') {
-        return 'InvalidDocument'
+        return 'InvalidProject'
     }
     return projectUri
 }
 
 async function findOpenLeanProjectUri(): Promise<FileUri | undefined | 'NoValidDocument'> {
-    const activeEditor = window.activeTextEditor
-    if (activeEditor) {
-        const projectUri = await findLean4DocumentProjectUri(activeEditor.document)
-        if (projectUri !== 'InvalidDocument') {
+    const activeEditor = lean.activeLeanEditor
+    if (activeEditor !== undefined) {
+        const projectUri = await findLeanEditorProjectUri(activeEditor)
+        if (projectUri !== 'InvalidProject') {
             return projectUri
         }
     }
 
     // This happens if vscode starts with a lean file open
     // but the "Getting Started" page is active.
-    for (const editor of window.visibleTextEditors) {
-        const projectUri = await findLean4DocumentProjectUri(editor.document)
-        if (projectUri !== 'InvalidDocument') {
+    for (const editor of lean.visibleLeanEditors) {
+        const projectUri = await findLeanEditorProjectUri(editor)
+        if (projectUri !== 'InvalidProject') {
             return projectUri
         }
     }
@@ -183,7 +180,7 @@ async function activateLean4Features(
     watchService.lakeFileChanged(packageUri => installer.handleLakeFileChanged(packageUri))
     context.subscriptions.push(watchService)
 
-    const infoProvider = new InfoProvider(clientProvider, { language: 'lean4' }, context)
+    const infoProvider = new InfoProvider(clientProvider, context)
     context.subscriptions.push(infoProvider)
 
     context.subscriptions.push(new LeanTaskGutter(clientProvider, context))
@@ -240,10 +237,10 @@ async function tryActivatingLean4Features(
     }
     context.subscriptions.push(
         onEventWhile(
-            leanEditor.onDidRevealLeanEditor,
+            lean.onDidRevealLeanEditor,
             withoutReentrancy('Continue', async editor => {
-                const projectUri = await findLean4DocumentProjectUri(editor.document)
-                if (projectUri === 'InvalidDocument') {
+                const projectUri = await findLeanEditorProjectUri(editor)
+                if (projectUri === 'InvalidProject') {
                     return 'Continue'
                 }
                 await tryActivatingLean4FeaturesInProject(context, installer, resolve, d, projectUri)