diff --git a/vscode-lean4/src/abbreviationview.ts b/vscode-lean4/src/abbreviationview.ts index c1913fc5..12a986f9 100644 --- a/vscode-lean4/src/abbreviationview.ts +++ b/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, diff --git a/vscode-lean4/src/diagnostics/fullDiagnostics.ts b/vscode-lean4/src/diagnostics/fullDiagnostics.ts index 4dc7a7a6..0f268c94 100644 --- a/vscode-lean4/src/diagnostics/fullDiagnostics.ts +++ b/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() diff --git a/vscode-lean4/src/extension.ts b/vscode-lean4/src/extension.ts index ab787df2..9230e202 100644 --- a/vscode-lean4/src/extension.ts +++ b/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 { - const docUri = toExtUri(doc.uri) - if (docUri === undefined || doc.languageId !== 'lean4') { - return 'InvalidDocument' - } +async function findLeanEditorProjectUri(editor: LeanEditor): Promise { + 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 { - 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) diff --git a/vscode-lean4/src/infoview.ts b/vscode-lean4/src/infoview.ts index b13c8a19..38e4dea1 100644 --- a/vscode-lean4/src/infoview.ts +++ b/vscode-lean4/src/infoview.ts @@ -14,17 +14,14 @@ import { commands, Diagnostic, Disposable, - DocumentSelector, env, ExtensionContext, - languages, Position, Range, Selection, TextEditor, TextEditorRevealType, Uri, - ViewColumn, WebviewPanel, window, workspace, @@ -51,8 +48,10 @@ import { Rpc } from './rpc' import { LeanClientProvider } from './utils/clientProvider' import { c2pConverter, p2cConverter } from './utils/converters' import { ExtUri, parseExtUri, toExtUri } from './utils/exturi' +import { lean, LeanEditor } from './utils/leanEditorProvider' import { logger } from './utils/logger' import { displayNotification } from './utils/notifs' +import { viewColumnOfActiveTextEditor, viewColumnOfInfoView } from './utils/viewColumn' const keepAlivePeriodMs = 10000 @@ -97,7 +96,6 @@ export class InfoProvider implements Disposable { private stylesheet: string = '' private autoOpened: boolean = false - private clientProvider: LeanClientProvider // Subscriptions are counted and only disposed of when count becomes 0. private serverNotifSubscriptions: Map = new Map() @@ -288,18 +286,7 @@ export class InfoProvider implements Disposable { if (extUri === undefined) { return } - - const client = this.clientProvider.findClient(extUri) - if (!client) { - return - } - - const document = workspace.textDocuments.find(doc => extUri.equalsUri(doc.uri)) - if (!document || document.isClosed) { - return - } - - await client.restartFile(document) + this.clientProvider.restartFile(extUri) }, createRpcSession: async uri => { @@ -329,28 +316,26 @@ export class InfoProvider implements Disposable { } constructor( - private provider: LeanClientProvider, - private readonly leanDocs: DocumentSelector, + private clientProvider: LeanClientProvider, private context: ExtensionContext, ) { - this.clientProvider = provider this.updateStylesheet() - provider.clientAdded(client => { + clientProvider.clientAdded(client => { void this.onClientAdded(client) }) - provider.clientRemoved(client => { + clientProvider.clientRemoved(client => { void this.onClientRemoved(client) }) - provider.clientStopped(([client, activeClient, reason]) => { + clientProvider.clientStopped(([client, activeClient, reason]) => { void this.onActiveClientStopped(client, activeClient, reason) }) this.subscriptions.push( - window.onDidChangeActiveTextEditor(() => this.sendPosition()), - window.onDidChangeTextEditorSelection(() => this.sendPosition()), + lean.onDidChangeActiveLeanEditor(() => this.sendPosition()), + lean.onDidChangeLeanEditorSelection(() => this.sendPosition()), workspace.onDidChangeConfiguration(async _e => { // regression; changing the style needs a reload. :/ this.updateStylesheet() @@ -359,13 +344,13 @@ export class InfoProvider implements Disposable { workspace.onDidChangeTextDocument(async () => { await this.sendPosition() }), - commands.registerTextEditorCommand('lean4.displayGoal', editor => this.openPreview(editor)), + lean.registerLeanEditorCommand('lean4.displayGoal', leanEditor => this.openPreview(leanEditor)), commands.registerCommand('lean4.toggleInfoview', () => this.toggleInfoview()), - commands.registerTextEditorCommand('lean4.displayList', async editor => { - await this.openPreview(editor) + lean.registerLeanEditorCommand('lean4.displayList', async leanEditor => { + await this.openPreview(leanEditor) await this.webviewPanel?.api.requestedAction({ kind: 'toggleAllMessages' }) }), - commands.registerTextEditorCommand('lean4.infoView.copyToComment', () => + lean.registerLeanEditorCommand('lean4.infoView.copyToComment', () => this.webviewPanel?.api.requestedAction({ kind: 'copyToComment' }), ), commands.registerCommand('lean4.infoView.toggleUpdating', () => @@ -374,7 +359,7 @@ export class InfoProvider implements Disposable { commands.registerCommand('lean4.infoView.toggleExpectedType', () => this.webviewPanel?.api.requestedAction({ kind: 'toggleExpectedType' }), ), - commands.registerTextEditorCommand('lean4.infoView.toggleStickyPosition', () => + lean.registerLeanEditorCommand('lean4.infoView.toggleStickyPosition', () => this.webviewPanel?.api.requestedAction({ kind: 'togglePin' }), ), commands.registerCommand('lean4.infoview.goToDefinition', args => @@ -414,7 +399,7 @@ export class InfoProvider implements Disposable { if (this.clientsFailed.has(folderUri.toString())) { this.clientsFailed.delete(folderUri.toString()) } - await this.initInfoView(window.activeTextEditor, client) + await this.initInfoView(lean.activeLeanEditor, client) } private async onClientAdded(client: LeanClient) { @@ -549,13 +534,10 @@ export class InfoProvider implements Disposable { } private async autoOpen(): Promise { - if (!this.webviewPanel && !this.autoOpened && getInfoViewAutoOpen() && window.activeTextEditor) { - // only auto-open for lean files, not for markdown. - if (languages.match(this.leanDocs, window.activeTextEditor.document)) { - // remember we've auto opened during this session so if user closes it it remains closed. - this.autoOpened = true - return await this.openPreview(window.activeTextEditor) - } + if (!this.webviewPanel && !this.autoOpened && getInfoViewAutoOpen() && lean.activeLeanEditor !== undefined) { + // remember we've auto opened during this session so if user closes it it remains closed. + this.autoOpened = true + return await this.openPreview(lean.activeLeanEditor) } return false } @@ -583,8 +565,8 @@ export class InfoProvider implements Disposable { if (this.webviewPanel) { this.webviewPanel.dispose() // the onDispose handler sets this.webviewPanel = undefined - } else if (window.activeTextEditor && window.activeTextEditor.document.languageId === 'lean4') { - await this.openPreview(window.activeTextEditor) + } else if (lean.activeLeanEditor !== undefined) { + await this.openPreview(lean.activeLeanEditor) } else { displayNotification( 'Error', @@ -593,23 +575,14 @@ export class InfoProvider implements Disposable { } } - private async openPreview(editor: TextEditor): Promise { - const docUri = toExtUri(editor.document.uri) - if (docUri === undefined) { - return false - } - - let column = editor && editor.viewColumn ? editor.viewColumn + 1 : ViewColumn.Two - if (column === 4) { - column = ViewColumn.Three - } + private async openPreview(leanEditor: LeanEditor): Promise { if (this.webviewPanel) { - this.webviewPanel.reveal(column, true) + this.webviewPanel.reveal(undefined, true) } else { const webviewPanel = window.createWebviewPanel( 'lean4_infoview', 'Lean Infoview', - { viewColumn: column, preserveFocus: true }, + { viewColumn: viewColumnOfInfoView(), preserveFocus: true }, { enableFindWidget: true, retainContextWhenHidden: true, @@ -649,15 +622,15 @@ export class InfoProvider implements Disposable { this.webviewPanel = webviewPanel webviewPanel.webview.html = this.initialHtml() - const client = this.clientProvider.findClient(docUri) - await this.initInfoView(editor, client) + const client = this.clientProvider.findClient(leanEditor.documentExtUri) + await this.initInfoView(leanEditor, client) } return true } - private async initInfoView(editor: TextEditor | undefined, client: LeanClient | undefined) { - if (editor) { - const loc = this.getLocation(editor) + private async initInfoView(leanEditor: LeanEditor | undefined, client: LeanClient | undefined) { + if (leanEditor !== undefined) { + const loc = this.getLocation(leanEditor) if (loc) { await this.webviewPanel?.api.initialize(loc) } @@ -737,12 +710,10 @@ export class InfoProvider implements Disposable { .catch(() => {}) } - private getLocation(editor: TextEditor): ls.Location | undefined { - if (!editor) return undefined - const uri = editor.document.uri - const selection = editor.selection + private getLocation(leanEditor: LeanEditor): ls.Location | undefined { + const selection = leanEditor.editor.selection return { - uri: uri.toString(), + uri: leanEditor.documentExtUri.toString(), range: { start: selection.start, end: selection.end, @@ -751,20 +722,12 @@ export class InfoProvider implements Disposable { } private async sendPosition() { - const editor = window.activeTextEditor - if (!editor) return - const loc = this.getLocation(editor) - if (languages.match(this.leanDocs, editor.document) === 0) { - // language is not yet 'lean4', but the LeanClient will fire the didSetLanguage event - // in openLean4Document and that's when we can send the position to update the - // InfoView for the newly opened document. - return - } - const uri = toExtUri(editor.document.uri) - if (uri === undefined) { + const editor = lean.activeLeanEditor + if (editor === undefined) { return } - // actual editor + const loc = this.getLocation(editor) + const uri = editor.documentExtUri if (this.clientsFailed.size > 0 || this.workersFailed.size > 0) { const client = this.clientProvider.findClient(uri) const uriKey = uri.toString() @@ -799,16 +762,12 @@ export class InfoProvider implements Disposable { } private async revealEditorSelection(uri: ExtUri, selection?: Range) { - let editor: TextEditor | undefined - for (const e of window.visibleTextEditors) { - if (uri.equalsUri(e.document.uri)) { - editor = e - break - } - } - if (!editor) { - const c = window.activeTextEditor ? window.activeTextEditor.viewColumn : ViewColumn.One - editor = await window.showTextDocument(uri.asUri(), { viewColumn: c, preserveFocus: false }) + let editor: TextEditor | undefined = lean.getVisibleLeanEditorsByUri(uri).at(0)?.editor + if (editor === undefined) { + editor = await window.showTextDocument(uri.asUri(), { + viewColumn: viewColumnOfActiveTextEditor(), + preserveFocus: false, + }) } if (selection !== undefined) { editor.revealRange(selection, TextEditorRevealType.InCenterIfOutsideViewport) @@ -824,22 +783,16 @@ export class InfoProvider implements Disposable { uri?: ExtUri | undefined, pos?: Position | undefined, ) { - let editor: TextEditor | undefined + let leanEditor: LeanEditor | undefined if (uri) { - editor = window.visibleTextEditors.find(e => uri.equalsUri(e.document.uri)) + leanEditor = lean.getVisibleLeanEditorsByUri(uri).at(0) } else { - editor = window.activeTextEditor - if (!editor) { - // sometimes activeTextEditor is null. - editor = window.visibleTextEditors.find(e => e.document.languageId === 'lean4') - } + leanEditor = lean.activeLeanEditor } - if (!editor) { - // user must have switch away from any lean source file in which case we don't know - // what to do here. TODO: show a popup error? Or should we use the last uri used in - // sendPosition and automatically activate that editor? + if (leanEditor === undefined) { return } + const editor = leanEditor.editor pos = pos ? pos : editor.selection.active if (kind === 'above') { // in this case, assume that we actually want to insert at the same diff --git a/vscode-lean4/src/leanclient.ts b/vscode-lean4/src/leanclient.ts index 6ab566d0..48dbb251 100644 --- a/vscode-lean4/src/leanclient.ts +++ b/vscode-lean4/src/leanclient.ts @@ -9,9 +9,7 @@ import { ProgressLocation, ProgressOptions, Range, - TextDocument, window, - workspace, WorkspaceFolder, } from 'vscode' import { @@ -43,6 +41,7 @@ import { logger } from './utils/logger' import { SemVer } from 'semver' import { c2pConverter, p2cConverter, patchConverters, setDependencyBuildMode } from './utils/converters' import { ExtUri, parseExtUri, toExtUri } from './utils/exturi' +import { lean, LeanDocument } from './utils/leanEditorProvider' import { displayNotification, displayNotificationWithOptionalInput, @@ -149,8 +148,8 @@ export class LeanClient implements Disposable { input: restartItem, action: () => { if (restartFile && uri !== undefined) { - const document = workspace.textDocuments.find(doc => uri.equalsUri(doc.uri)) - if (document) { + const document = lean.getLeanDocumentByUri(uri) + if (document !== undefined) { void this.restartFile(document) } } else { @@ -305,8 +304,8 @@ export class LeanClient implements Disposable { { input, action: () => { - const document = workspace.textDocuments.find(doc => fileUri.equalsUri(doc.uri)) - if (!document || document.isClosed) { + const document = lean.getLeanDocumentByUri(fileUri) + if (document === undefined) { displayNotification( 'Error', `'${fileName}' was closed in the meantime. Imports will not be rebuilt.`, @@ -388,26 +387,21 @@ export class LeanClient implements Disposable { this.running = false } - async restartFile(doc: TextDocument): Promise { + async restartFile(leanDoc: LeanDocument): Promise { if (this.client === undefined || !this.running) return // there was a problem starting lean server. - const docUri = toExtUri(doc.uri) - if (docUri === undefined) { + if (!this.isInFolderManagedByThisClient(leanDoc.extUri)) { return } - if (!this.isInFolderManagedByThisClient(docUri)) { - return - } - - const uri = docUri.toString() + const uri = leanDoc.extUri.toString() if (!this.openServerDocuments.delete(uri)) { return } logger.log(`[LeanClient] Restarting File: ${uri}`) await this.client.sendNotification( 'textDocument/didClose', - this.client.code2ProtocolConverter.asCloseTextDocumentParams(doc), + this.client.code2ProtocolConverter.asCloseTextDocumentParams(leanDoc.doc), ) if (this.openServerDocuments.has(uri)) { @@ -416,7 +410,7 @@ export class LeanClient implements Disposable { this.openServerDocuments.add(uri) await this.client.sendNotification( 'textDocument/didOpen', - setDependencyBuildMode(this.client.code2ProtocolConverter.asOpenTextDocumentParams(doc), 'once'), + setDependencyBuildMode(this.client.code2ProtocolConverter.asOpenTextDocumentParams(leanDoc.doc), 'once'), ) this.restartedWorkerEmitter.fire(uri) diff --git a/vscode-lean4/src/loogleview.ts b/vscode-lean4/src/loogleview.ts index 6b5a8336..b9ef52ea 100644 --- a/vscode-lean4/src/loogleview.ts +++ b/vscode-lean4/src/loogleview.ts @@ -1,6 +1,7 @@ -import { Disposable, ViewColumn, WebviewPanel, commands, version, window } from 'vscode' +import { Disposable, WebviewPanel, commands, version, window } from 'vscode' import { VSCodeAbbreviationConfig } from './abbreviation/VSCodeAbbreviationConfig' import { FileUri } from './utils/exturi' +import { viewColumnOfInfoView } from './utils/viewColumn' function escapeHtml(s: string) { return s @@ -30,17 +31,10 @@ export class LoogleView implements Disposable { } async display(initialQuery?: string | undefined) { - let column = - window.activeTextEditor && window.activeTextEditor?.viewColumn - ? window.activeTextEditor?.viewColumn + 1 - : ViewColumn.Two - if (column === 4) { - column = ViewColumn.Three - } const webviewPanel = window.createWebviewPanel( 'lean4_loogleview', 'LoogleView', - { viewColumn: column }, + { viewColumn: viewColumnOfInfoView() }, { enableScripts: true, enableFindWidget: true, diff --git a/vscode-lean4/src/manualview.ts b/vscode-lean4/src/manualview.ts index ec795751..4ddea178 100644 --- a/vscode-lean4/src/manualview.ts +++ b/vscode-lean4/src/manualview.ts @@ -1,8 +1,9 @@ import { promises as fs } from 'fs' import markdownit from 'markdown-it' import anchor from 'markdown-it-anchor' -import { Disposable, Uri, ViewColumn, WebviewPanel, commands, window } from 'vscode' +import { Disposable, Uri, WebviewPanel, commands, window } from 'vscode' import { FileUri } from './utils/exturi' +import { viewColumnOfActiveTextEditor } from './utils/viewColumn' export class ManualView implements Disposable { private subscriptions: Disposable[] = [] @@ -25,7 +26,7 @@ export class ManualView implements Disposable { this.webviewPanel = window.createWebviewPanel( 'lean4_manualview', 'Lean 4 VS Code Extension Manual', - { viewColumn: window.activeTextEditor?.viewColumn ?? ViewColumn.One }, + { viewColumn: viewColumnOfActiveTextEditor() }, { enableFindWidget: true, enableCommandUris: true, diff --git a/vscode-lean4/src/moogleview.ts b/vscode-lean4/src/moogleview.ts index 632f4b79..935ed116 100644 --- a/vscode-lean4/src/moogleview.ts +++ b/vscode-lean4/src/moogleview.ts @@ -1,6 +1,7 @@ -import { Disposable, ViewColumn, WebviewPanel, commands, version, window } from 'vscode' +import { Disposable, WebviewPanel, commands, version, window } from 'vscode' import { VSCodeAbbreviationConfig } from './abbreviation/VSCodeAbbreviationConfig' import { FileUri } from './utils/exturi' +import { viewColumnOfInfoView } from './utils/viewColumn' function escapeHtml(s: string) { return s @@ -26,17 +27,10 @@ export class MoogleView implements Disposable { } async display() { - let column = - window.activeTextEditor && window.activeTextEditor?.viewColumn - ? window.activeTextEditor?.viewColumn + 1 - : ViewColumn.Two - if (column === 4) { - column = ViewColumn.Three - } const webviewPanel = window.createWebviewPanel( 'lean4_moogleview', 'MoogleView', - { viewColumn: column }, + { viewColumn: viewColumnOfInfoView() }, { enableScripts: true, enableFindWidget: true, diff --git a/vscode-lean4/src/projectoperations.ts b/vscode-lean4/src/projectoperations.ts index 0d5f3050..f990f8e8 100644 --- a/vscode-lean4/src/projectoperations.ts +++ b/vscode-lean4/src/projectoperations.ts @@ -4,8 +4,8 @@ import { commands, Disposable, OutputChannel, QuickPickItem, window } from 'vsco import { LeanClient } from './leanclient' import { batchExecute, displayResultError, ExecutionExitCode, ExecutionResult } from './utils/batch' import { LeanClientProvider } from './utils/clientProvider' -import { toExtUri } from './utils/exturi' import { cacheNotFoundError, lake, LakeRunner } from './utils/lake' +import { lean } from './utils/leanEditorProvider' import { DirectGitDependency, Manifest, ManifestReadError, parseManifestInFolder } from './utils/manifest' import { displayNotification, displayNotificationWithInput, displayNotificationWithOptionalInput } from './utils/notifs' @@ -128,23 +128,17 @@ export class ProjectOperationProvider implements Disposable { await this.runOperation('Fetch Mathlib Build Cache For Current Imports', async lakeRunner => { const projectUri = lakeRunner.cwdUri! - if (!window.activeTextEditor || window.activeTextEditor.document.languageId !== 'lean4') { + const doc = lean.lastActiveLeanDocument + if (doc === undefined) { displayNotification( 'Error', 'No active Lean editor tab. Make sure to focus the Lean editor tab for which you want to fetch the cache.', ) return } + const docUri = doc.extUri - const activeFileUri = toExtUri(window.activeTextEditor.document.uri) - if (activeFileUri === undefined) { - displayNotification( - 'Error', - `Cannot fetch cache of file with invalid URI kind: ${window.activeTextEditor.document.uri}`, - ) - return - } - if (activeFileUri.scheme === 'untitled') { + if (docUri.scheme === 'untitled') { displayNotification('Error', 'Cannot fetch cache of untitled files.') return } @@ -166,36 +160,33 @@ export class ProjectOperationProvider implements Disposable { if (projectName !== 'mathlib') { displayNotification( 'Error', - "Cache of focused file can only be fetched in Mathlib itself. Use the 'Project: Fetch Mathlib Build Cache' command for fetching the full Mathlib build cache in projects depending on Mathlib.", + "Cache for current imports can only be fetched in Mathlib itself. Use the 'Project: Fetch Mathlib Build Cache' command for fetching the full Mathlib build cache in projects depending on Mathlib.", ) return } - const relativeActiveFileUri = activeFileUri.relativeTo(projectUri) - if (relativeActiveFileUri === undefined) { + const relativeDocUri = docUri.relativeTo(projectUri) + if (relativeDocUri === undefined) { displayNotification( 'Error', - `Cannot fetch cache of focused file: focused file (${activeFileUri.fsPath}) is not contained in active project folder (${projectUri.fsPath}).`, + `Cannot fetch cache for current imports: active file (${docUri.fsPath}) is not contained in active project folder (${projectUri.fsPath}).`, ) return } - const result: ExecutionResult = await lakeRunner.fetchMathlibCacheForFile(relativeActiveFileUri) + const result: ExecutionResult = await lakeRunner.fetchMathlibCacheForFile(relativeDocUri) if (result.exitCode === ExecutionExitCode.Cancelled) { return } if (result.exitCode !== ExecutionExitCode.Success) { - displayResultError( - result, - `Cannot fetch Mathlib build artifact cache for '${relativeActiveFileUri.fsPath}'.`, - ) + displayResultError(result, `Cannot fetch Mathlib build artifact cache for '${relativeDocUri.fsPath}'.`) return } displayNotificationWithOptionalInput( 'Information', - `Mathlib build artifact cache for '${relativeActiveFileUri.fsPath}' fetched successfully.`, - [{ input: 'Restart File', action: () => this.clientProvider.restartFile(activeFileUri) }], + `Mathlib build artifact cache for '${relativeDocUri.fsPath}' fetched successfully.`, + [{ input: 'Restart File', action: () => this.clientProvider.restartFile(relativeDocUri) }], ) }) } diff --git a/vscode-lean4/src/taskgutter.ts b/vscode-lean4/src/taskgutter.ts index ec220e28..580be6a8 100644 --- a/vscode-lean4/src/taskgutter.ts +++ b/vscode-lean4/src/taskgutter.ts @@ -1,12 +1,14 @@ import { LeanFileProgressKind, LeanFileProgressProcessingInfo } from '@leanprover/infoview-api' import { Disposable, ExtensionContext, OverviewRulerLane, Range, TextEditorDecorationType, window } from 'vscode' import { LeanClientProvider } from './utils/clientProvider' +import { ExtUri } from './utils/exturi' +import { lean } from './utils/leanEditorProvider' class LeanFileTaskGutter { private timeout?: NodeJS.Timeout constructor( - private uri: string, + private uri: ExtUri, private decorations: Map, private processed: LeanFileProgressProcessingInfo[], ) { @@ -41,22 +43,19 @@ class LeanFileTaskGutter { } private updateDecos() { - for (const editor of window.visibleTextEditors) { - if (editor.document.uri.toString() === this.uri) { - for (const [kind, [decoration, message]] of this.decorations) { - editor.setDecorations( - decoration, - this.processed - .filter( - info => - (info.kind === undefined ? LeanFileProgressKind.Processing : info.kind) === kind, - ) - .map(info => ({ - range: new Range(info.range.start.line, 0, info.range.end.line, 0), - hoverMessage: message, - })), - ) - } + for (const leanEditor of lean.getVisibleLeanEditorsByUri(this.uri)) { + for (const [kind, [decoration, message]] of this.decorations) { + leanEditor.editor.setDecorations( + decoration, + this.processed + .filter( + info => (info.kind === undefined ? LeanFileProgressKind.Processing : info.kind) === kind, + ) + .map(info => ({ + range: new Range(info.range.start.line, 0, info.range.end.line, 0), + hoverMessage: message, + })), + ) } } } @@ -106,7 +105,7 @@ export class LeanTaskGutter implements Disposable { ]) this.subscriptions.push( - window.onDidChangeVisibleTextEditors(() => this.updateDecos()), + lean.onDidChangeVisibleLeanEditors(() => this.updateDecos()), client.progressChanged(([uri, processing]) => { this.status[uri] = processing this.updateDecos() @@ -116,16 +115,15 @@ export class LeanTaskGutter implements Disposable { private updateDecos() { const uris: { [uri: string]: boolean } = {} - for (const editor of window.visibleTextEditors) { - if (editor.document.languageId !== 'lean4') continue - const uri = editor.document.uri.toString() + for (const editor of lean.visibleLeanEditors) { + const uri = editor.documentExtUri.toString() uris[uri] = true const processed = uri in this.status ? this.status[uri] : [] if (this.gutters[uri]) { const gutter = this.gutters[uri] if (gutter) gutter.setProcessed(processed) } else { - this.gutters[uri] = new LeanFileTaskGutter(uri, this.decorations, processed) + this.gutters[uri] = new LeanFileTaskGutter(editor.documentExtUri, this.decorations, processed) } } for (const uri of Object.getOwnPropertyNames(this.gutters)) { diff --git a/vscode-lean4/src/utils/clientProvider.ts b/vscode-lean4/src/utils/clientProvider.ts index cb39dbb4..5c58fdc5 100644 --- a/vscode-lean4/src/utils/clientProvider.ts +++ b/vscode-lean4/src/utils/clientProvider.ts @@ -1,10 +1,11 @@ import { LeanFileProgressProcessingInfo, ServerStoppedReason } from '@leanprover/infoview-api' import path from 'path' -import { Disposable, EventEmitter, OutputChannel, TextDocument, commands, window, workspace } from 'vscode' +import { Disposable, EventEmitter, OutputChannel, commands, workspace } from 'vscode' import { SetupDiagnostics, checkAll } from '../diagnostics/setupDiagnostics' import { PreconditionCheckResult, SetupNotificationOptions } from '../diagnostics/setupNotifs' import { LeanClient } from '../leanclient' -import { ExtUri, FileUri, UntitledUri, getWorkspaceFolderUri, toExtUri } from './exturi' +import { ExtUri, FileUri, UntitledUri, getWorkspaceFolderUri } from './exturi' +import { lean } from './leanEditorProvider' import { LeanInstaller } from './leanInstaller' import { logger } from './logger' import { displayNotification } from './notifs' @@ -62,13 +63,14 @@ export class LeanClientProvider implements Disposable { // we must setup the installChanged event handler first before any didOpenEditor calls. installer.installChanged(async (uri: FileUri) => await this.onInstallChanged(uri)) - window.visibleTextEditors.forEach(e => this.didOpenEditor(e.document)) + lean.visibleLeanEditors.forEach(e => this.ensureClient(e.documentExtUri)) + this.subscriptions.push( - window.onDidChangeActiveTextEditor(async e => { - if (!e) { + lean.onDidChangeActiveLeanEditor(async e => { + if (e === undefined) { return } - await this.didOpenEditor(e.document) + await this.ensureClient(e.documentExtUri) }), ) @@ -79,7 +81,7 @@ export class LeanClientProvider implements Disposable { commands.registerCommand('lean4.stopServer', () => this.stopActiveClient()), ) - workspace.onDidOpenTextDocument(document => this.didOpenEditor(document)) + lean.onDidOpenLeanDocument(document => this.ensureClient(document.extUri)) workspace.onDidChangeWorkspaceFolders(event => { // Remove all clients that are not referenced by any folder anymore @@ -153,8 +155,8 @@ export class LeanClientProvider implements Disposable { return } - const doc = workspace.textDocuments.find(doc => uri.equalsUri(doc.uri)) - if (!doc) { + const doc = lean.getLeanDocumentByUri(uri) + if (doc === undefined) { displayNotification('Error', `'${fileName}' was closed in the meantime.`) return } @@ -163,20 +165,15 @@ export class LeanClientProvider implements Disposable { } restartActiveFile() { - if (!this.activeClient || !this.activeClient.isRunning()) { - displayNotification('Error', 'No active client.') - return - } - - if (!window.activeTextEditor || window.activeTextEditor.document.languageId !== 'lean4') { + const doc = lean.lastActiveLeanDocument + if (doc === undefined) { displayNotification( 'Error', 'No active Lean editor tab. Make sure to focus the Lean editor tab for which you want to issue a restart.', ) return } - - void this.activeClient.restartFile(window.activeTextEditor.document) + this.restartFile(doc.extUri) } private stopActiveClient() { @@ -193,20 +190,6 @@ export class LeanClientProvider implements Disposable { void this.activeClient?.isStarted() } - async didOpenEditor(document: TextDocument) { - // bail as quickly as possible on non-lean files. - if (document.languageId !== 'lean4') { - return - } - - const uri = toExtUri(document.uri) - if (uri === undefined) { - return - } - - await this.ensureClient(uri) - } - // Find the client for a given document. findClient(path: ExtUri) { const candidates = this.getClients().filter(client => client.isInFolderManagedByThisClient(path)) diff --git a/vscode-lean4/src/utils/leanEditorProvider.ts b/vscode-lean4/src/utils/leanEditorProvider.ts index 102a7f0c..e7f52496 100644 --- a/vscode-lean4/src/utils/leanEditorProvider.ts +++ b/vscode-lean4/src/utils/leanEditorProvider.ts @@ -1,5 +1,16 @@ -import { Disposable, EventEmitter, ExtensionContext, TextDocument, TextEditor, Uri, window, workspace } from 'vscode' -import { ExtUri, isExtUri } from './exturi' +import { + commands, + Disposable, + EventEmitter, + ExtensionContext, + TextDocument, + TextEditor, + TextEditorEdit, + TextEditorSelectionChangeEvent, + window, + workspace, +} from 'vscode' +import { ExtUri, isExtUri, toExtUriOrError } from './exturi' function groupByKey(values: V[], key: (value: V) => K): Map { const r = new Map() @@ -20,30 +31,80 @@ function groupByUniqueKey(values: V[], key: (value: V) => K): Map { return r } -class TextDocumentIndex { - private docsByUri: Map +export class LeanDocument { + constructor( + readonly doc: TextDocument, + readonly extUri: ExtUri, + ) {} + + equals(other: LeanDocument): boolean { + return this.doc === other.doc + } + + equalsTextDocument(other: TextDocument): boolean { + return this.doc === other + } + + static equalsWithUndefined(a: LeanDocument | undefined, b: LeanDocument | undefined): boolean { + if (a === undefined) { + return b === undefined + } + if (b === undefined) { + return a === undefined + } + return a.equals(b) + } +} + +export class LeanEditor { + constructor( + readonly editor: TextEditor, + readonly documentExtUri: ExtUri, + ) {} + + equals(other: LeanEditor): boolean { + return this.editor === other.editor + } + + equalsTextEditor(other: TextEditor): boolean { + return this.editor === other + } + + static equalsWithUndefined(a: LeanEditor | undefined, b: LeanEditor | undefined): boolean { + if (a === undefined) { + return b === undefined + } + if (b === undefined) { + return a === undefined + } + return a.equals(b) + } +} + +class LeanDocumentIndex { + private docsByUri: Map /** - * Assumes that `docs` only contains at most one `TextDocument` per URI. + * Assumes that `docs` only contains at most one `LeanDocument` per URI. * This is given for `TextDocument`s from VS Code. * */ - constructor(docs: TextDocument[]) { - this.docsByUri = groupByUniqueKey(docs, doc => doc.uri.toString()) + constructor(docs: LeanDocument[]) { + this.docsByUri = groupByUniqueKey(docs, doc => doc.extUri.toString()) } - get(uri: Uri): TextDocument | undefined { + get(uri: ExtUri): LeanDocument | undefined { return this.docsByUri.get(uri.toString()) } } -class TextEditorIndex { - private editorsByUri: Map +class LeanEditorIndex { + private editorsByUri: Map - constructor(editors: TextEditor[]) { - this.editorsByUri = groupByKey(editors, editor => editor.document.uri.toString()) + constructor(editors: LeanEditor[]) { + this.editorsByUri = groupByKey(editors, editor => editor.documentExtUri.toString()) } - get(uri: Uri): TextEditor[] | undefined { + get(uri: ExtUri): LeanEditor[] | undefined { return this.editorsByUri.get(uri.toString()) } } @@ -52,76 +113,93 @@ export function isLeanDocument(doc: TextDocument): boolean { return isExtUri(doc.uri) && doc.languageId === 'lean4' } -export function filterLeanDocuments(docs: readonly TextDocument[]): TextDocument[] { - return docs.filter(doc => isLeanDocument(doc)) +export function asLeanDocument(doc: TextDocument): LeanDocument | undefined { + if (isLeanDocument(doc)) { + return new LeanDocument(doc, toExtUriOrError(doc.uri)) + } + return undefined +} + +export function filterLeanDocuments(docs: readonly TextDocument[]): LeanDocument[] { + return docs.map(doc => asLeanDocument(doc)).filter(doc => doc !== undefined) } -export function filterLeanDocument(doc: TextDocument | undefined): TextDocument | undefined { - if (doc !== undefined && isLeanDocument(doc)) { - return doc +export function filterLeanDocument(doc: TextDocument | undefined): LeanDocument | undefined { + if (doc === undefined) { + return undefined } - return undefined + return asLeanDocument(doc) } export function isLeanEditor(editor: TextEditor): boolean { return isLeanDocument(editor.document) } -export function filterLeanEditors(editors: readonly TextEditor[]): TextEditor[] { - return editors.filter(editor => isLeanEditor(editor)) +export function asLeanEditor(editor: TextEditor): LeanEditor | undefined { + if (isLeanEditor(editor)) { + return new LeanEditor(editor, toExtUriOrError(editor.document.uri)) + } + return undefined +} + +export function filterLeanEditors(editors: readonly TextEditor[]): LeanEditor[] { + return editors.map(editor => asLeanEditor(editor)).filter(editor => editor !== undefined) } -export function filterLeanEditor(editor: TextEditor | undefined): TextEditor | undefined { - if (editor !== undefined && isLeanEditor(editor)) { - return editor +export function filterLeanEditor(editor: TextEditor | undefined): LeanEditor | undefined { + if (editor === undefined) { + return undefined } - return undefined + return asLeanEditor(editor) } export class LeanEditorProvider implements Disposable { private subscriptions: Disposable[] = [] - private _visibleLeanEditors: TextEditor[] - private visibleLeanEditorsByUri: TextEditorIndex - private readonly onDidChangeVisibleLeanEditorsEmitter = new EventEmitter() + private _visibleLeanEditors: LeanEditor[] + private visibleLeanEditorsByUri: LeanEditorIndex + private readonly onDidChangeVisibleLeanEditorsEmitter = new EventEmitter() readonly onDidChangeVisibleLeanEditors = this.onDidChangeVisibleLeanEditorsEmitter.event - private _activeLeanEditor: TextEditor | undefined - private readonly onDidChangeActiveLeanEditorEmitter = new EventEmitter() + private _activeLeanEditor: LeanEditor | undefined + private readonly onDidChangeActiveLeanEditorEmitter = new EventEmitter() readonly onDidChangeActiveLeanEditor = this.onDidChangeActiveLeanEditorEmitter.event - private _lastActiveLeanEditor: TextEditor | undefined - private readonly onDidChangeLastActiveLeanEditorEmitter = new EventEmitter() + private _lastActiveLeanEditor: LeanEditor | undefined + private readonly onDidChangeLastActiveLeanEditorEmitter = new EventEmitter() readonly onDidChangeLastActiveLeanEditor = this.onDidChangeLastActiveLeanEditorEmitter.event - private _leanDocuments: TextDocument[] - private leanDocumentsByUri: TextDocumentIndex - private readonly onDidChangeLeanDocumentsEmitter = new EventEmitter() + private _leanDocuments: LeanDocument[] + private leanDocumentsByUri: LeanDocumentIndex + private readonly onDidChangeLeanDocumentsEmitter = new EventEmitter() readonly onDidChangeLeanDocuments = this.onDidChangeLeanDocumentsEmitter.event - private readonly onDidOpenLeanDocumentEmitter = new EventEmitter() + private readonly onDidOpenLeanDocumentEmitter = new EventEmitter() readonly onDidOpenLeanDocument = this.onDidOpenLeanDocumentEmitter.event - private readonly onDidCloseLeanDocumentEmitter = new EventEmitter() + private readonly onDidCloseLeanDocumentEmitter = new EventEmitter() readonly onDidCloseLeanDocument = this.onDidCloseLeanDocumentEmitter.event - private _lastActiveLeanDocument: TextDocument | undefined - private readonly onDidChangeLastActiveLeanDocumentEmitter = new EventEmitter() + private _lastActiveLeanDocument: LeanDocument | undefined + private readonly onDidChangeLastActiveLeanDocumentEmitter = new EventEmitter() readonly onDidChangeLastActiveLeanDocument = this.onDidChangeLastActiveLeanDocumentEmitter.event - private readonly onDidRevealLeanEditorEmitter = new EventEmitter() + private readonly onDidRevealLeanEditorEmitter = new EventEmitter() readonly onDidRevealLeanEditor = this.onDidRevealLeanEditorEmitter.event - private readonly onDidConcealLeanEditorEmitter = new EventEmitter() + private readonly onDidConcealLeanEditorEmitter = new EventEmitter() readonly onDidConcealLeanEditor = this.onDidConcealLeanEditorEmitter.event + private readonly onDidChangeLeanEditorSelectionEmitter = new EventEmitter() + readonly onDidChangeLeanEditorSelection = this.onDidChangeLeanEditorSelectionEmitter.event + constructor() { this._visibleLeanEditors = filterLeanEditors(window.visibleTextEditors) - this.visibleLeanEditorsByUri = new TextEditorIndex(this._visibleLeanEditors) + this.visibleLeanEditorsByUri = new LeanEditorIndex(this._visibleLeanEditors) this.subscriptions.push(window.onDidChangeVisibleTextEditors(editors => this.updateVisibleTextEditors(editors))) this._activeLeanEditor = filterLeanEditor(window.activeTextEditor) this.subscriptions.push(window.onDidChangeActiveTextEditor(editor => this.updateActiveTextEditor(editor))) this._leanDocuments = filterLeanDocuments(workspace.textDocuments) - this.leanDocumentsByUri = new TextDocumentIndex(this._leanDocuments) + this.leanDocumentsByUri = new LeanDocumentIndex(this._leanDocuments) this.subscriptions.push( workspace.onDidOpenTextDocument(doc => { this.updateLeanDocuments(workspace.textDocuments) @@ -134,15 +212,16 @@ export class LeanEditorProvider implements Disposable { ) this.subscriptions.push( workspace.onDidCloseTextDocument(doc => { - this.updateLeanDocuments(workspace.textDocuments) - this.closeLeanDocument(doc) - this.invalidateClosedLastActiveLeanDocument(doc) // Update visible and active editors in case this `onDidCloseTextDocument` call was // triggered by a changed language ID. this.updateVisibleTextEditors(window.visibleTextEditors) this.updateActiveTextEditor(window.activeTextEditor) + this.updateLeanDocuments(workspace.textDocuments) + this.closeLeanDocument(doc) + this.invalidateClosedLastActiveLeanDocument(doc) }), ) + this.subscriptions.push(window.onDidChangeTextEditorSelection(event => this.updateTextEditorSelection(event))) } private updateVisibleTextEditors(visibleTextEditors: readonly TextEditor[]) { @@ -163,25 +242,25 @@ export class LeanEditorProvider implements Disposable { const newVisibleLeanEditors = filterLeanEditors(visibleTextEditors) if ( newVisibleLeanEditors.length === this._visibleLeanEditors.length && - newVisibleLeanEditors.every( - (newVisibleLeanEditor, i) => newVisibleLeanEditor === this._visibleLeanEditors[i], + newVisibleLeanEditors.every((newVisibleLeanEditor, i) => + newVisibleLeanEditor.equals(this._visibleLeanEditors[i]), ) ) { return } this._visibleLeanEditors = newVisibleLeanEditors - this.visibleLeanEditorsByUri = new TextEditorIndex(newVisibleLeanEditors) + this.visibleLeanEditorsByUri = new LeanEditorIndex(newVisibleLeanEditors) this.onDidChangeVisibleLeanEditorsEmitter.fire(newVisibleLeanEditors) } private revealLeanEditors( - oldVisibleLeanEditors: readonly TextEditor[], + oldVisibleLeanEditors: readonly LeanEditor[], newVisibleTextEditors: readonly TextEditor[], ) { - const oldVisibleLeanEditorsIndex = new Set(oldVisibleLeanEditors) + const oldVisibleLeanEditorsIndex = new Set(oldVisibleLeanEditors.map(leanEditor => leanEditor.editor)) const newVisibleLeanEditors = filterLeanEditors(newVisibleTextEditors) const revealedLeanEditors = newVisibleLeanEditors.filter( - newVisibleLeanEditor => !oldVisibleLeanEditorsIndex.has(newVisibleLeanEditor), + newVisibleLeanEditor => !oldVisibleLeanEditorsIndex.has(newVisibleLeanEditor.editor), ) for (const revealedLeanEditor of revealedLeanEditors) { this.onDidRevealLeanEditorEmitter.fire(revealedLeanEditor) @@ -189,13 +268,13 @@ export class LeanEditorProvider implements Disposable { } private concealLeanEditors( - oldVisibleLeanEditors: readonly TextEditor[], + oldVisibleLeanEditors: readonly LeanEditor[], newVisibleTextEditors: readonly TextEditor[], ) { const newVisibleLeanEditors = filterLeanEditors(newVisibleTextEditors) - const newVisibleLeanEditorsIndex = new Set(newVisibleLeanEditors) + const newVisibleLeanEditorsIndex = new Set(newVisibleLeanEditors.map(leanEditor => leanEditor.editor)) const concealedLeanEditors = oldVisibleLeanEditors.filter( - newVisibleLeanEditor => !newVisibleLeanEditorsIndex.has(newVisibleLeanEditor), + newVisibleLeanEditor => !newVisibleLeanEditorsIndex.has(newVisibleLeanEditor.editor), ) for (const concealedLeanEditor of concealedLeanEditors) { this.onDidConcealLeanEditorEmitter.fire(concealedLeanEditor) @@ -204,7 +283,7 @@ export class LeanEditorProvider implements Disposable { private updateActiveLeanEditor(activeTextEditor: TextEditor | undefined) { const newActiveLeanEditor = filterLeanEditor(activeTextEditor) - if (newActiveLeanEditor === this._activeLeanEditor) { + if (LeanEditor.equalsWithUndefined(newActiveLeanEditor, this._activeLeanEditor)) { return } this._activeLeanEditor = newActiveLeanEditor @@ -212,7 +291,10 @@ export class LeanEditorProvider implements Disposable { } private invalidateInvisibleLastActiveLeanEditor(visibleTextEditors: readonly TextEditor[]) { - if (this._lastActiveLeanEditor !== undefined && !visibleTextEditors.includes(this._lastActiveLeanEditor)) { + if ( + this._lastActiveLeanEditor !== undefined && + !visibleTextEditors.includes(this._lastActiveLeanEditor.editor) + ) { this._lastActiveLeanEditor = undefined this.onDidChangeLastActiveLeanEditorEmitter.fire(undefined) } @@ -223,7 +305,7 @@ export class LeanEditorProvider implements Disposable { if (newLastActiveLeanEditor === undefined) { return } - if (newLastActiveLeanEditor === this._lastActiveLeanEditor) { + if (LeanEditor.equalsWithUndefined(newLastActiveLeanEditor, this._lastActiveLeanEditor)) { return } this._lastActiveLeanEditor = newLastActiveLeanEditor @@ -234,12 +316,12 @@ export class LeanEditorProvider implements Disposable { const newLeanDocuments = filterLeanDocuments(textDocuments) if ( newLeanDocuments.length === this._leanDocuments.length && - newLeanDocuments.every((newLeanDocument, i) => newLeanDocument === this._leanDocuments[i]) + newLeanDocuments.every((newLeanDocument, i) => newLeanDocument.equals(this._leanDocuments[i])) ) { return } this._leanDocuments = newLeanDocuments - this.leanDocumentsByUri = new TextDocumentIndex(newLeanDocuments) + this.leanDocumentsByUri = new LeanDocumentIndex(newLeanDocuments) this.onDidChangeLeanDocumentsEmitter.fire(newLeanDocuments) } @@ -260,7 +342,7 @@ export class LeanEditorProvider implements Disposable { } private invalidateClosedLastActiveLeanDocument(closedTextDocument: TextDocument) { - if (this._lastActiveLeanDocument === closedTextDocument) { + if (this._lastActiveLeanDocument?.doc === closedTextDocument) { this._lastActiveLeanDocument = undefined this.onDidChangeLastActiveLeanDocumentEmitter.fire(undefined) } @@ -271,39 +353,64 @@ export class LeanEditorProvider implements Disposable { if (newLastActiveLeanDocument === undefined) { return } - if (newLastActiveLeanDocument === this._lastActiveLeanDocument) { + if (LeanDocument.equalsWithUndefined(newLastActiveLeanDocument, this._lastActiveLeanDocument)) { return } this._lastActiveLeanDocument = newLastActiveLeanDocument this.onDidChangeLastActiveLeanDocumentEmitter.fire(newLastActiveLeanDocument) } - get visibleLeanEditors(): readonly TextEditor[] { + private updateTextEditorSelection(event: TextEditorSelectionChangeEvent) { + if (!isLeanEditor(event.textEditor)) { + return + } + this.onDidChangeLeanEditorSelectionEmitter.fire(event) + } + + get visibleLeanEditors(): readonly LeanEditor[] { return this._visibleLeanEditors } - get activeLeanEditor(): TextEditor | undefined { + get activeLeanEditor(): LeanEditor | undefined { return this._activeLeanEditor } - get lastActiveLeanEditor(): TextEditor | undefined { + get lastActiveLeanEditor(): LeanEditor | undefined { return this._lastActiveLeanEditor } - get leanDocuments(): readonly TextDocument[] { + get leanDocuments(): readonly LeanDocument[] { return this._leanDocuments } - get lastActiveLeanDocument(): TextDocument | undefined { + get lastActiveLeanDocument(): LeanDocument | undefined { return this._lastActiveLeanDocument } - getVisibleLeanEditorsByUri(uri: ExtUri): readonly TextEditor[] | undefined { - return this.visibleLeanEditorsByUri.get(uri.asUri()) + getVisibleLeanEditorsByUri(uri: ExtUri): readonly LeanEditor[] { + return this.visibleLeanEditorsByUri.get(uri) ?? [] } - getLeanDocumentByUri(uri: ExtUri): TextDocument | undefined { - return this.leanDocumentsByUri.get(uri.asUri()) + getLeanDocumentByUri(uri: ExtUri): LeanDocument | undefined { + return this.leanDocumentsByUri.get(uri) + } + + registerLeanEditorCommand( + command: string, + callback: (leanEditor: LeanEditor, edit: TextEditorEdit, ...args: any[]) => void, + thisArg?: any, + ): Disposable { + return commands.registerTextEditorCommand( + command, + (editor, edit, ...args) => { + const leanEditor = filterLeanEditor(editor) + if (leanEditor === undefined) { + return + } + callback(leanEditor, edit, ...args) + }, + thisArg, + ) } dispose() { @@ -313,10 +420,10 @@ export class LeanEditorProvider implements Disposable { } } -export let leanEditor: LeanEditorProvider +export let lean: LeanEditorProvider /** Must be called at the very start when the extension is activated so that `leanEditor` is defined. */ export function registerLeanEditor(context: ExtensionContext) { - leanEditor = new LeanEditorProvider() - context.subscriptions.push(leanEditor) + lean = new LeanEditorProvider() + context.subscriptions.push(lean) } diff --git a/vscode-lean4/src/utils/notifs.ts b/vscode-lean4/src/utils/notifs.ts index f5565b3e..12036eb0 100644 --- a/vscode-lean4/src/utils/notifs.ts +++ b/vscode-lean4/src/utils/notifs.ts @@ -1,6 +1,6 @@ /* eslint-disable @typescript-eslint/no-redundant-type-constituents */ import { Disposable, MessageOptions, commands, window } from 'vscode' -import { leanEditor } from './leanEditorProvider' +import { lean } from './leanEditorProvider' // All calls to window.show(Error|Warning|Information)... should go through functions in this file // to prevent accidentally blocking the VS Code extension. @@ -88,7 +88,7 @@ function makeSticky(n: StickyNotification): Disposable { } } - d = leanEditor.onDidRevealLeanEditor(async () => await display()) + d = lean.onDidRevealLeanEditor(async () => await display()) void display() diff --git a/vscode-lean4/src/utils/viewColumn.ts b/vscode-lean4/src/utils/viewColumn.ts new file mode 100644 index 00000000..b1fadb9a --- /dev/null +++ b/vscode-lean4/src/utils/viewColumn.ts @@ -0,0 +1,17 @@ +import { TabInputWebview, ViewColumn, window } from 'vscode' + +export function viewColumnOfInfoView(): ViewColumn { + for (const tabGroup of window.tabGroups.all) { + const tab = tabGroup.tabs.find( + tab => tab.input instanceof TabInputWebview && tab.input.viewType === 'mainThreadWebview-lean4_infoview', + ) + if (tab !== undefined) { + return tabGroup.viewColumn + } + } + return ViewColumn.Beside +} + +export function viewColumnOfActiveTextEditor(): ViewColumn { + return window.activeTextEditor?.viewColumn ?? ViewColumn.One +}