diff --git a/.gitmodules b/.gitmodules index 1f2b97bc..c9f7a251 100644 --- a/.gitmodules +++ b/.gitmodules @@ -1,6 +1,6 @@ [submodule "Projects/lean4web-tools"] path = Projects/lean4web-tools url = https://github.com/hhu-adam/lean4web-tools.git -[submodule "client/vscode-lean4"] - path = client/vscode-lean4 - url = https://github.com/leanprover/vscode-lean4.git +[submodule "client/monaco-lean4"] + path = client/monaco-lean4 + url = git@github.com:hhu-adam/monaco-lean4.git diff --git a/client/monaco-lean4 b/client/monaco-lean4 new file mode 160000 index 00000000..f0187e26 --- /dev/null +++ b/client/monaco-lean4 @@ -0,0 +1 @@ +Subproject commit f0187e2641dd08eb668c9bfff1be996eb7bfd9a4 diff --git a/client/src/Editor.tsx b/client/src/Editor.tsx index feef1ade..b805c01d 100644 --- a/client/src/Editor.tsx +++ b/client/src/Editor.tsx @@ -3,11 +3,11 @@ import { useEffect, useRef, useState } from 'react' import * as monaco from 'monaco-editor/esm/vs/editor/editor.api.js' import { loadRenderInfoview } from '@leanprover/infoview/loader' import { InfoviewApi } from '@leanprover/infoview-api' -import { InfoProvider } from './editor/infoview' -import { LeanClient } from './editor/leanclient' -import { AbbreviationRewriter } from './editor/abbreviation/rewriter/AbbreviationRewriter' -import { AbbreviationProvider } from './editor/abbreviation/AbbreviationProvider' -import { LeanTaskGutter } from './editor/taskgutter' +import { InfoProvider } from '../monaco-lean4/vscode-lean4/src/infoview' +import { LeanClient } from '../monaco-lean4/vscode-lean4/src/leanclient' +import { AbbreviationRewriter } from '../monaco-lean4/vscode-lean4/src/abbreviation/rewriter/AbbreviationRewriter' +import { AbbreviationProvider } from '../monaco-lean4/vscode-lean4/src/abbreviation/AbbreviationProvider' +import { LeanTaskGutter } from '../monaco-lean4/vscode-lean4/src/taskgutter' import Split from 'react-split' import Notification from './Notification' import settings from './config/settings' @@ -17,9 +17,10 @@ import { DisposingWebSocketMessageReader } from './reader' import { monacoSetup } from './monacoSetup' import './css/Editor.css' -import './editor/infoview.css' -import './editor/vscode.css' +import './css/infoview.css' +import './css/vscode.css' import { render } from '@testing-library/react' +import { AbbreviationConfig } from '../monaco-lean4/vscode-lean4/src/abbreviation/config' monacoSetup() @@ -96,7 +97,8 @@ const Editor: React.FC<{setRestart?, onDidChangeContent?, value: string, theme: wrappingStrategy: "advanced", }) setEditor(editor) - const abbrevRewriter = new AbbreviationRewriter(new AbbreviationProvider(), model, editor) + + const abbrevRewriter = new AbbreviationRewriter(new AbbreviationProvider(AbbreviationConfig), model, editor) return () => { editor.dispose(); model.dispose(); @@ -184,7 +186,6 @@ const Editor: React.FC<{setRestart?, onDidChangeContent?, value: string, theme: setRestart((project?) => restart) }, [editor, infoviewApi, infoProvider]) - return (
+Date: Wed May 29 15:52:58 2024 +0200 + + add vscode-lean4 as submodule + +commit c06471c81129dbad2f8a7cbd2718b2f1b79127de (origin/dev) +Author: Jon Eugster +Date: Tue May 7 12:20:09 2024 +0200 + + many things + +commit 3cc8a85d28bf42ca3254f1458b725f77251d33d0 +Author: Jon Eugster +Date: Thu May 2 17:18:45 2024 +0200 + + temp. add entire vscode-lean4 extension + +commit 013dbada1fd2557ce5d25b8fd88f32aba1ce8e41 +Author: Jon Eugster +Date: Thu May 2 04:06:56 2024 +0200 + + cleanup App.tsx and config + + + + + + + + + + + + + +commit 5e2ea468ab9401eb0d5d16efbde21bbe9cc6521f +Author: Jon Eugster +Date: Thu May 2 02:32:02 2024 +0200 + + cleanup navigation. includes #12. + +commit 012f97aa23a1a516171c075b6f45ad7be789e2b0 +Author: Jon Eugster +Date: Tue Apr 30 17:29:49 2024 +0200 + + cleanup App.tsx, part 2 + +commit 30055c00891c2caff8a8446feee78766c1807063 +Author: Jon Eugster +Date: Tue Apr 30 17:17:35 2024 +0200 + + cleanup App.tsx, part 1 + +commit 182ba518ea89d046914b3242e97dc4cc9974944f +Author: Jon Eugster +Date: Tue Apr 30 17:17:04 2024 +0200 + + fix updated infoview + +commit 88d83ea6b1cd0885c9fcd19223d629ddf507af44 +Author: Jon Eugster +Date: Mon Apr 29 20:30:14 2024 +0200 + + temporarily use my own npm packages instead diff --git a/client/src/config/editor.json b/client/src/config/editor.json new file mode 100644 index 00000000..963c835b --- /dev/null +++ b/client/src/config/editor.json @@ -0,0 +1,23 @@ +{ + "glyphMargin": true, + "lineDecorationsWidth": 5, + "folding": false, + "lineNumbers": "on", + "lineNumbersMinChars": 1, + "rulers": [100], + "lightbulb": { + "enabled": true + }, + "unicodeHighlight": { + "ambiguousCharacters": false + }, + "automaticLayout": true, + "minimap": { + "enabled": false + }, + "tabSize": 2, + "semanticHighlighting.enabled": true, + "theme": "vs", + "fontFamily": "JuliaMono", + "wrappingStrategy": "advanced" +} diff --git a/client/src/editor/infoview.css b/client/src/css/infoview.css similarity index 100% rename from client/src/editor/infoview.css rename to client/src/css/infoview.css diff --git a/client/src/editor/vscode.css b/client/src/css/vscode.css similarity index 100% rename from client/src/editor/vscode.css rename to client/src/css/vscode.css diff --git a/client/src/editor/abbreviation/AbbreviationHoverProvider.ts b/client/src/editor/abbreviation/AbbreviationHoverProvider.ts deleted file mode 100644 index 81422481..00000000 --- a/client/src/editor/abbreviation/AbbreviationHoverProvider.ts +++ /dev/null @@ -1,49 +0,0 @@ -/* This file is based on `vscode-lean4/vscode-lean4/src/abbreviation/AbbreviationHoverProvider.ts` */ - -import { AbbreviationProvider } from './AbbreviationProvider'; -import settings from '../../config/settings'; -import * as monaco from 'monaco-editor/esm/vs/editor/editor.api.js' - -/** - * Adds hover behaviour for getting translations of unicode characters. - * Eg: "Type ⊓ using \glb or \sqcap" - */ -export class AbbreviationHoverProvider implements monaco.languages.HoverProvider { - constructor( - private readonly abbreviations: AbbreviationProvider - ) {} - - provideHover(model: monaco.editor.ITextModel, pos: monaco.Position): monaco.languages.Hover | undefined { - const context = model.getLineContent(pos.lineNumber).substring(pos.column-1); - const symbolsAtCursor = this.abbreviations.findSymbolsIn(context); - const allAbbrevs = symbolsAtCursor.map((symbol) => ({ - symbol, - abbrevs: this.abbreviations.getAllAbbreviations(symbol), - })); - - if ( - allAbbrevs.length === 0 || - allAbbrevs.every((a) => a.abbrevs.length === 0) - ) { - return undefined; - } - - const leader = settings.abbreviationCharacter; - - const hoverMarkdown = allAbbrevs - .map( - ({ symbol, abbrevs }) => - `Type ${symbol} using ${abbrevs - .map((a) => '`' + leader + a + '`') - .join(' or ')}` - ) - .join('\n\n'); - - const maxSymbolLength = Math.max( - ...allAbbrevs.map((a) => a.symbol.length) - ); - const hoverRange = new monaco.Range(pos.lineNumber, pos.column-1, pos.lineNumber, pos.column-1 + maxSymbolLength); - - return {contents: [{value: hoverMarkdown}], range: hoverRange}; - } -} diff --git a/client/src/editor/abbreviation/AbbreviationProvider.ts b/client/src/editor/abbreviation/AbbreviationProvider.ts deleted file mode 100644 index 7b656d1c..00000000 --- a/client/src/editor/abbreviation/AbbreviationProvider.ts +++ /dev/null @@ -1,108 +0,0 @@ -/* This file is based on `vscode-lean4/vscode-lean4/src/abbreviation/AbbreviationProvider.ts` */ - -import { computed } from 'mobx'; -// import { Disposable } from 'vscode'; -// import { autorunDisposable } from '../utils/autorunDisposable'; -import abbreviations from '../../../vscode-lean4/vscode-lean4/src/abbreviation/abbreviations.json'; -import settings from '../../config/settings'; - -export interface SymbolsByAbbreviation { - [abbrev: string]: string; -} - -/** - * Answers queries to a database of abbreviations. - */ -export class AbbreviationProvider { - // private readonly disposables = new Array(); - private cache: Record = {}; - - constructor() { - // this.disposables.push( - // autorunDisposable(() => { - // // For the livetime of this component, cache the computed's - // const _ = this.symbolsByAbbreviation; - // // clear cache on change - // this.cache = {}; - // }) - // ); - } - - private get symbolsByAbbreviation(): SymbolsByAbbreviation { - // There are only like 1000 symbols. Building an index is not required yet. - return { - ...abbreviations, - ...settings.inputModeCustomTranslations - }; - } - - getAllAbbreviations(symbol: string): string[] { - return Object.entries(this.symbolsByAbbreviation) - .filter(([abbr, sym]) => sym === symbol) - .map(([abbr]) => abbr); - } - - findSymbolsIn(symbolPlusUnknown: string): string[] { - const result = new Set(); - for (const [abbr, sym] of Object.entries(this.symbolsByAbbreviation)) { - if (symbolPlusUnknown.startsWith(sym)) { - result.add(sym); - } - } - return [...result.values()]; - } - - /** - * Computes the replacement text for a typed abbreviation (excl. leader). - * This converts the longest non-empty prefix with the best-matching abbreviation. - * - * For example: - * getReplacementText("alp") returns "α" - * getReplacementText("alp7") returns "α7" - * getReplacementText("") returns undefined - */ - getReplacementText(abbrev: string): string | undefined { - if (abbrev in this.cache) { - return this.cache[abbrev]; - } - const result = this._getReplacementText(abbrev); - this.cache[abbrev] = result; - return result; - } - - private _getReplacementText(abbrev: string): string | undefined { - if (abbrev.length === 0) { - return undefined; - } - - const matchingSymbol = this.findSymbolsByAbbreviationPrefix(abbrev)[0]; - if (matchingSymbol) { - return matchingSymbol; - } - - // Convert the `alp` in `\alp7` - const prefixReplacement = this.getReplacementText( - abbrev.slice(0, abbrev.length - 1) - ); - if (prefixReplacement) { - return prefixReplacement + abbrev.slice(abbrev.length - 1); - } - - return undefined; - } - - getSymbolForAbbreviation(abbrev: string): string | undefined { - return this.symbolsByAbbreviation[abbrev]; - } - - findSymbolsByAbbreviationPrefix(abbrevPrefix: string): string[] { - const matchingAbbreviations = Object.keys( - this.symbolsByAbbreviation - ).filter((abbrev) => abbrev.startsWith(abbrevPrefix)); - - matchingAbbreviations.sort((a, b) => a.length - b.length); - return matchingAbbreviations.map( - (abbr) => this.symbolsByAbbreviation[abbr] - ); - } -} diff --git a/client/src/editor/abbreviation/rewriter/AbbreviationRewriter.ts b/client/src/editor/abbreviation/rewriter/AbbreviationRewriter.ts deleted file mode 100644 index 28a36065..00000000 --- a/client/src/editor/abbreviation/rewriter/AbbreviationRewriter.ts +++ /dev/null @@ -1,278 +0,0 @@ -/* This file is based on `vscode-lean4/vscode-lean4/src/abbreviation/rewriter/AbbreviationRewriter.ts` */ - -// import { Range as LineColRange } from 'vscode'; -import { Disposable } from 'vscode'; -import { assert } from '../../../../vscode-lean4/vscode-lean4/src/utils/assert'; -import { AbbreviationProvider } from '../AbbreviationProvider'; -import { Range } from '../../../../vscode-lean4/vscode-lean4/src/abbreviation/rewriter/Range'; -import settings from '../../../config/settings'; -import { TrackedAbbreviation } from './TrackedAbbreviation'; -import * as monaco from 'monaco-editor/esm/vs/editor/editor.api.js' -import {IRange, Range as MonacoRange} from 'monaco-editor' -import { AbbreviationHoverProvider } from '../AbbreviationHoverProvider'; - -/** - * Tracks abbreviations in a given text editor and replaces them when dynamically. - */ -export class AbbreviationRewriter { - private readonly disposables = new Array(); - // /** - // * All tracked abbreviations are disjoint. - // */ - private readonly trackedAbbreviations = new Set(); - // private readonly decorationType = window.createTextEditorDecorationType({ - // textDecoration: 'underline', - // }); - - private dontTrackNewAbbr = false; - private decosIds: string[] = []; - // private isActiveContextKey: monaco.editor.IContextKey; - abbreviationHoverProvider: AbbreviationHoverProvider; - // private stderrOutput: OutputChannel; - // private firstOutput = true; - - constructor( - private readonly abbreviationProvider: AbbreviationProvider, - private readonly model: monaco.editor.ITextModel, - private readonly editor: monaco.editor.IStandaloneCodeEditor - ) { - this.disposables.push(model.onDidChangeContent((e: monaco.editor.IModelContentChangedEvent) => { - const changes = e.changes.slice(0); - // // We need to process the changes at the bottom first. - // // Otherwise, changes at the top will move spans at the bottom down. - changes.sort((c1, c2) => c2.rangeOffset - c1.rangeOffset); - - for (const c of changes) { - const range = new Range(c.rangeOffset, c.rangeLength); - this.processChange(range, c.text); - } - - this.updateState(); - - // // Replace any tracked abbreviation that is either finished or unique. - void this.forceReplace( - [...this.trackedAbbreviations].filter( - (abbr) => - abbr.finished || - (settings.eagerReplacementEnabled && - abbr.isAbbreviationUniqueAndComplete) - ) - ); - })) - - - this.disposables.push( - editor.onDidChangeCursorSelection((e: monaco.editor.ICursorSelectionChangedEvent) => { - // Replace any tracked abbreviation that lost selection. - void this.forceReplace( - [...this.trackedAbbreviations].filter( - (abbr) => - ![...e.secondarySelections, e.selection].some((s) => - abbr.range.containsRange( - fromVsCodeRange( - s, - this.model - ).withLength(0) - ) - ) - ) - ); - }) - ) - - // this.isActiveContextKey = this.editor.createContextKey('lean4.input.isActive', false); - - this.disposables.push( - monaco.editor.addEditorAction({ - id: 'lean4.input.convert', - label: 'Convert abbreviation', - precondition: "editorTextFocus && editorLangId == lean4 && lean4.input.isActive", - keybindings: [monaco.KeyCode.Tab], - run: async () => this.forceReplace([...this.trackedAbbreviations]) - }) - ) - - this.abbreviationHoverProvider = new AbbreviationHoverProvider(this.abbreviationProvider) - - this.disposables.push( - monaco.languages.registerHoverProvider('lean4', this.abbreviationHoverProvider) - ) - } - - private async forceReplace( - abbreviations: TrackedAbbreviation[] - ): Promise { - if (abbreviations.length === 0) { - return; - } - for (const a of abbreviations) { - this.trackedAbbreviations.delete(a); - } - - // Wait for VS Code to trigger `onDidChangeTextEditorSelection` - await waitForNextTick(); - - const cursorVar = '$CURSOR'; - const replacements = new Array<{ - range: Range; - newText: string; - transformOffsetInRange: (offset: number) => number; - }>(); - for (const abbr of abbreviations) { - const symbol = abbr.matchingSymbol; - if (symbol) { - const newText = symbol.replace(cursorVar, ''); - let cursorOffset = symbol.indexOf(cursorVar); - if (cursorOffset === -1) { - // position the cursor after the inserted symbol - cursorOffset = newText.length; - } - replacements.push({ - range: abbr.range, - newText, - transformOffsetInRange: (offset) => cursorOffset, - }); - } - } - // Process replacements with highest offset first - replacements.sort((a, b) => b.range.offset - a.range.offset); - - // We cannot rely on VS Code to update the selections - - // it becomes janky if symbols are inserted that are longer - // than their abbreviation. It also does not really work for \[[]]. - const newSelections = this.editor.getSelections() - .map((s) => ({range: fromVsCodeRange(s, this.model), dir: s.getDirection()})) - .map(({range: s, dir}) => { - // Apply the replacement of abbreviations to the selections. - let newSel = s; - for (const r of replacements) { - if ( - r.range.isBefore(newSel) && - !r.range.containsRange(newSel) - ) { - // don't do this on ` \abbr| ` - newSel = newSel.move(r.newText.length - r.range.length); - } else if ( - !r.range.isAfter(newSel) || - r.range.containsRange(newSel) - ) { - // do this on ` \abbr| ` or ` \ab|br ` - // newSel and r.range intersect - const offset = newSel.offset - r.range.offset; - const newOffset = r.transformOffsetInRange(offset); - newSel = newSel.move(newOffset - offset); - } - } - return {range: newSel, dir}; - }); - - // We don't want replaced symbols (e.g. "\") to trigger abbreviations. - this.dontTrackNewAbbr = true; - let ok = false; - try { - await this.editor.pushUndoStop() - await this.editor.executeEdits("abbreviation-rewriter", - replacements.map((r) => { - return { - range: toVsCodeRange(r.range, this.model), - text: r.newText - } - })); - - ok = true - } catch (e) { - throw Error('Error: while replacing abbreviation: ' + e); - } - this.dontTrackNewAbbr = false; - - if (ok) { - this.editor.setSelections(newSelections.map(({range: s, dir}) => { - const vr = toVsCodeRange(s, this.model); - return monaco.Selection.fromRange(vr, dir); - })); - - // this.abbreviationProvider.onAbbreviationsCompleted(this.textEditor); - } - else { - // Our edit did not succeed, do not update the selections. - // This can happen if `waitForNextTick` waits too long. - throw Error('Error: Unable to replace abbreviation'); - } - - this.updateState(); - } - - private updateState() { - this.decosIds = this.model.deltaDecorations(this.decosIds, - [...this.trackedAbbreviations].map((a: TrackedAbbreviation) => { - return { - range: toVsCodeRange(a.range, this.model), - options: { - inlineClassName: 'abbreviation' - } - }})) - - // void this.setInputActive(this.trackedAbbreviations.size > 0); - } - - // private async setInputActive(isActive: boolean) { - // this.isActiveContextKey.set(isActive); - // } - - private processChange( - range: Range, - text: string - ): { affectedAbbr: TrackedAbbreviation | undefined } { - let affectedAbbr: TrackedAbbreviation | undefined; - for (const abbr of [...this.trackedAbbreviations]) { - const { isAffected, shouldStopTracking } = abbr.processChange( - range, - text - ); - if (isAffected) { - // At most one abbreviation should be affected - assert(() => !affectedAbbr); - affectedAbbr = abbr; - } - if (shouldStopTracking) { - this.trackedAbbreviations.delete(abbr); - } - } - - if ( - text === settings.abbreviationCharacter && - !affectedAbbr && - !this.dontTrackNewAbbr - ) { - const abbr = new TrackedAbbreviation( - new Range(range.offset + 1, 0), - '', - this.abbreviationProvider - ); - this.trackedAbbreviations.add(abbr); - } - return { affectedAbbr }; - } - - dispose(): void { - for (const d of this.disposables) { - d.dispose(); - } - } -} - -function fromVsCodeRange(range: IRange, model: monaco.editor.ITextModel): Range { - const start = model.getOffsetAt(MonacoRange.getStartPosition(range)); - const end = model.getOffsetAt(MonacoRange.getEndPosition(range)); - return new Range(start, end - start); -} - -function toVsCodeRange(range: Range, model: monaco.editor.ITextModel): monaco.Range { - const start = model.getPositionAt(range.offset); - const end = model.getPositionAt(range.offsetEnd + 1); - return MonacoRange.fromPositions(start, end); -} - -function waitForNextTick(): Promise { - return new Promise((res) => setTimeout(res, 0)); -} diff --git a/client/src/editor/abbreviation/rewriter/TrackedAbbreviation.ts b/client/src/editor/abbreviation/rewriter/TrackedAbbreviation.ts deleted file mode 100644 index 540bd380..00000000 --- a/client/src/editor/abbreviation/rewriter/TrackedAbbreviation.ts +++ /dev/null @@ -1,111 +0,0 @@ -// import { AbbreviationProvider } from '../AbbreviationProvider'; -import { AbbreviationProvider } from '../AbbreviationProvider'; -import { Range } from '../../../../vscode-lean4/vscode-lean4/src/abbreviation/rewriter/Range'; -/* This file is based on `vscode-lean4/vscode-lean4/src/abbreviation/rewriter/TrackedAbbreviation.ts` */ - -/** - * Represents an abbreviation that is tracked and currently typed by the user. - * When the multi-cursor feature is used, multiple abbreviations can be tracked at once. - */ -export class TrackedAbbreviation { - private _abbreviationRange: Range; - - get abbreviationRange(): Range { - return this._abbreviationRange; - } - - get range(): Range { - return this.abbreviationRange.moveKeepEnd(-1); - } - - get abbreviation(): string { - return this._text; - } - - get matchingSymbol(): string | undefined { - return this.abbreviationProvider.getReplacementText(this.abbreviation); - } - - /** - * Does this abbreviation uniquely identify a symbol and is it complete? - */ - get isAbbreviationUniqueAndComplete(): boolean { - return ( - this.abbreviation !== "" && // Check empty string for speed up - this.abbreviationProvider.findSymbolsByAbbreviationPrefix( - this.abbreviation - ).length === 1 && - !!this.abbreviationProvider.getSymbolForAbbreviation( - this.abbreviation - ) - ); - } - - private _finished = false; - /** - * Indicates whether this abbreviation has been continued with non-abbreviation characters. - * Such abbreviations should be replaced immediately. - */ - get finished(): boolean { - return this._finished; - } - - constructor( - abbreviationRange: Range, - private _text: string, - private readonly abbreviationProvider: AbbreviationProvider - ) { - this._abbreviationRange = abbreviationRange; - } - - processChange( - range: Range, - newText: string - ): { shouldStopTracking: boolean; isAffected: boolean } { - if (this.abbreviationRange.containsRange(range)) { - this._finished = false; - - if (this.abbreviationRange.isBefore(range)) { - // `newText` is appended to `this.abbreviation` - if ( - this.abbreviationProvider.findSymbolsByAbbreviationPrefix( - this.abbreviation + newText - ).length === 0 - ) { - // newText is not helpful anymore. Finish this and don't accept the change. - this._finished = true; - return { - shouldStopTracking: false, - isAffected: false, - }; - } - } - - this._abbreviationRange = this.abbreviationRange.moveEnd( - newText.length - range.length - ); - const startStr = this.abbreviation.substr( - 0, - range.offset - this.abbreviationRange.offset - ); - const endStr = this.abbreviation.substr( - range.offsetEnd + 1 - this.abbreviationRange.offset - ); - this._text = startStr + newText + endStr; - - return { shouldStopTracking: false, isAffected: true }; - } else if (range.isBefore(this.range)) { - // The changed happened before us. We need to move. - this._abbreviationRange = this._abbreviationRange.move( - newText.length - range.length - ); - return { shouldStopTracking: false, isAffected: false }; - } else if (range.isAfter(this.range)) { - // The change does not affect us. - return { shouldStopTracking: false, isAffected: false }; - } else { - // We cannot process the change. Abort tracking. - return { shouldStopTracking: true, isAffected: false }; - } - } -} diff --git a/client/src/editor/codicon.ttf b/client/src/editor/codicon.ttf deleted file mode 100644 index 1095acb9..00000000 Binary files a/client/src/editor/codicon.ttf and /dev/null differ diff --git a/client/src/editor/config.ts b/client/src/editor/config.ts deleted file mode 100644 index 998e6d0d..00000000 --- a/client/src/editor/config.ts +++ /dev/null @@ -1,5 +0,0 @@ -/* This file is based on `vscode-lean4/src/config.ts` */ - -export function getElaborationDelay(): number { - return 200 -} diff --git a/client/src/editor/infoview.ts b/client/src/editor/infoview.ts deleted file mode 100644 index 7790140b..00000000 --- a/client/src/editor/infoview.ts +++ /dev/null @@ -1,580 +0,0 @@ -/* This file is based on `vscode-lean4/vscode-lean4/src/infoview.ts ` */ - -import { - Disposable, Uri, window, workspace, Position -} from 'vscode' -import { - EditorApi, InfoviewApi, LeanFileProgressParams, TextInsertKind, - RpcConnectParams, RpcConnected, RpcKeepAliveParams, RpcErrorCode -} from '@leanprover/infoview-api' -import { LeanClient } from './leanclient' -import * as ls from 'vscode-languageserver-protocol' -import { c2pConverter, fromLanguageServerPosition, fromLanguageServerRange, p2cConverter, toLanguageServerRange } from './utils/converters' -// import { logger } from './utils/logger' -import * as monaco from 'monaco-editor/esm/vs/editor/editor.api.js' - -const keepAlivePeriodMs = 10000 - -async function rpcConnect (client: LeanClient, uri: ls.DocumentUri): Promise { - const connParams: RpcConnectParams = { uri } - const result: RpcConnected = await client.sendRequest('$/lean/rpc/connect', connParams) - return result.sessionId -} - -class RpcSessionAtPos implements Disposable { - keepAliveInterval?: NodeJS.Timeout - client: LeanClient - - constructor (client: LeanClient, public sessionId: string, public uri: ls.DocumentUri) { - this.client = client - this.keepAliveInterval = setInterval(async () => { - const params: RpcKeepAliveParams = { uri, sessionId } - try { - await client.sendNotification('$/lean/rpc/keepAlive', params) - } catch (e) { - console.log(`[InfoProvider] failed to send keepalive for ${uri}: ${e}`) - if (this.keepAliveInterval != null) clearInterval(this.keepAliveInterval) - } - }, keepAlivePeriodMs) - } - - dispose () { - if (this.keepAliveInterval != null) clearInterval(this.keepAliveInterval) - // TODO: at this point we could close the session - } -} - -export class InfoProvider implements Disposable { - /** Instance of the panel, if it is open. Otherwise `undefined`. */ - private infoviewApi?: InfoviewApi - private editor?: monaco.editor.IStandaloneCodeEditor - private readonly subscriptions: Disposable[] = [] - private readonly clientSubscriptions: Disposable[] = [] - - public readonly client?: LeanClient - // private readonly clientProvider: LeanClientProvider - - // Subscriptions are counted and only disposed of when count becomes 0. - private readonly serverNotifSubscriptions: Map = new Map() - private readonly clientNotifSubscriptions: Map = new Map() - - private rpcSessions: Map = new Map() - - // the key is the uri of the file who's worker has failed. - private readonly workersFailed: Map = new Map() - - private subscribeDidChangeNotification (client: LeanClient, method: string) { - const h = client.didChange((params) => { - void this.infoviewApi?.sentClientNotification(method, params) - }) - return h - } - - private subscribeDidCloseNotification (client: LeanClient, method: string) { - const h = client.didClose((params) => { - void this.infoviewApi?.sentClientNotification(method, params) - }) - return h - } - - private subscribeDiagnosticsNotification (client: LeanClient, method: string) { - const h = client.diagnostics((params) => { - void this.infoviewApi?.gotServerNotification(method, params) - }) - return h - } - - private subscribeCustomNotification (client: LeanClient, method: string) { - const h = client.customNotification(({ method: thisMethod, params }) => { - if (thisMethod !== method) return - void this.infoviewApi?.gotServerNotification(method, params) - }) - return h - } - - private readonly editorApi: EditorApi = { - sendClientRequest: async (uri: string, method: string, params: any): Promise => { - const client = this.client // clientProvider.findClient(uri) - if (client != null) { - try { - const result = await client.sendRequest(method, params) - return result - } catch (ex: any) { - if (ex.code === RpcErrorCode.WorkerCrashed) { - // ex codes related with worker exited or crashed - console.log(`[InfoProvider]The Lean Server has stopped processing this file: ${ex.message}`) - await this.onWorkerStopped(uri, client, { message: 'The Lean Server has stopped processing this file: ', reason: ex.message as string }) - } - throw ex - } - } - return undefined - }, - sendClientNotification: async (uri: string, method: string, params: any): Promise => { - const client = this.client // this.clientProvider.findClient(uri) - if (client != null) { - await client.sendNotification(method, params) - } - }, - subscribeServerNotifications: async (method) => { - const el = this.serverNotifSubscriptions.get(method) - if (el != null) { - const [count, h] = el - this.serverNotifSubscriptions.set(method, [count + 1, h]) - return - } - - // NOTE(WN): For non-custom notifications we cannot call LanguageClient.onNotification - // here because that *overwrites* the notification handler rather than registers an extra one. - // So we have to add a bunch of event emitters to `LeanClient.` - if (method === 'textDocument/publishDiagnostics') { - const subscriptions: Disposable[] = [] - for (const client of [this.client]/* this.clientProvider.getClients() */) { - subscriptions.push(this.subscribeDiagnosticsNotification(client!, method)) - } - this.serverNotifSubscriptions.set(method, [1, subscriptions]) - } else if (method.startsWith('$')) { - const subscriptions: Disposable[] = [] - for (const client of [this.client]/* this.clientProvider.getClients() */) { - subscriptions.push(this.subscribeCustomNotification(client!, method)) - } - this.serverNotifSubscriptions.set(method, [1, subscriptions]) - } else { - throw new Error(`subscription to ${method} server notifications not implemented`) - } - }, - unsubscribeServerNotifications: async (method) => { - const el = this.serverNotifSubscriptions.get(method) - if (el == null) return - const [count, subscriptions] = el - if (count === 1) { - for (const h of subscriptions) { - h.dispose() - } - this.serverNotifSubscriptions.delete(method) - } else { - this.serverNotifSubscriptions.set(method, [count - 1, subscriptions]) - } - }, - - subscribeClientNotifications: async (method) => { - const el = this.clientNotifSubscriptions.get(method) - if (el != null) { - const [count, d] = el - this.clientNotifSubscriptions.set(method, [count + 1, d]) - return - } - - if (method === 'textDocument/didChange') { - const subscriptions: Disposable[] = [] - for (const client of [this.client]/* this.clientProvider.getClients() */) { - subscriptions.push(this.subscribeDidChangeNotification(client!, method)) - } - this.clientNotifSubscriptions.set(method, [1, subscriptions]) - } else if (method === 'textDocument/didClose') { - const subscriptions: Disposable[] = [] - for (const client of [this.client]/* this.clientProvider.getClients() */) { - subscriptions.push(this.subscribeDidCloseNotification(client!, method)) - } - this.clientNotifSubscriptions.set(method, [1, subscriptions]) - } else { - throw new Error(`Subscription to '${method}' client notifications not implemented`) - } - }, - - unsubscribeClientNotifications: async (method) => { - const el = this.clientNotifSubscriptions.get(method) - if (el == null) return - const [count, subscriptions] = el - if (count === 1) { - for (const d of subscriptions) { - d.dispose() - } - this.clientNotifSubscriptions.delete(method) - } else { - this.clientNotifSubscriptions.set(method, [count - 1, subscriptions]) - } - }, - copyToClipboard: async (text) => { - navigator.clipboard.writeText(text) - }, - insertText: async (text, kind, tdpp) => { - let uri: Uri | undefined - let pos: Position | undefined - if (tdpp != null) { - uri = p2cConverter.asUri(tdpp.textDocument.uri) - pos = fromLanguageServerPosition(tdpp.position) - } - await this.handleInsertText(text, kind, uri, pos) - }, - applyEdit: async (e: ls.WorkspaceEdit) => { - const we = await p2cConverter.asWorkspaceEdit(e) - await workspace.applyEdit(we) - }, - showDocument: async (show) => { - void this.revealEditorSelection( - Uri.parse(show.uri), - fromLanguageServerRange(show.selection) - ) - }, - restartFile: async uri => { - - return // TODO! - - - // const extUri = parseExtUri(uri) - // 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) - }, - createRpcSession: async uri => { - const client = this.client // this.clientProvider.findClient(uri) - if (client == null) return '' - const sessionId = await rpcConnect(client, uri) - const session = new RpcSessionAtPos(client, sessionId, uri) - // if (this.webviewPanel == null) { - // session.dispose() - // throw Error('infoview disconnect while connecting to RPC session') - // } else { - this.rpcSessions.set(sessionId, session) - return sessionId - // } - }, - closeRpcSession: async sessionId => { - const session = this.rpcSessions.get(sessionId) - if (session != null) { - this.rpcSessions.delete(sessionId) - session.dispose() - } - } - } - - constructor (private readonly myclient: LeanClient | undefined) { - // this.clientProvider = provider - this.client = myclient - - this.onClientAdded(this.client!) - - this.subscriptions.push( - window.onDidChangeActiveTextEditor(async () => await this.sendPosition()), - window.onDidChangeTextEditorSelection(async () => await this.sendPosition()), - workspace.onDidChangeConfiguration(async (_e) => { - // regression; changing the style needs a reload. :/ - await this.sendConfig() - }), - workspace.onDidChangeTextDocument(async () => { - await this.sendPosition() - }) - ) - } - - private async onClientRestarted (client: LeanClient) { - // if we already have subscriptions for a previous client, we need to also - // subscribe to the same things on this new client. - for (const [method, [count, subscriptions]] of this.clientNotifSubscriptions) { - if (method === 'textDocument/didChange') { - subscriptions.push(this.subscribeDidChangeNotification(client, method)) - } else if (method === 'textDocument/didClose') { - subscriptions.push(this.subscribeDidCloseNotification(client, method)) - } - } - - for (const [method, [count, subscriptions]] of this.serverNotifSubscriptions) { - if (method === 'textDocument/publishDiagnostics') { - subscriptions.push(this.subscribeDiagnosticsNotification(client, method)) - } else if (method.startsWith('$')) { - subscriptions.push(this.subscribeCustomNotification(client, method)) - } - } - - await this.initInfoView(this.editor, client) - } - - private async onClientAdded (client: LeanClient) { - console.log(`[InfoProvider] Adding client`) - - this.clientSubscriptions.push( - client.restarted(async () => { - console.log('[InfoProvider] got client restarted event') - // This event is triggered both the first time the server starts - // as well as when the server restarts. - - this.clearRpcSessions(client) - - // Need to fully re-initialize this newly restarted client with all the - // existing subscriptions and resend position info and so on so the - // infoview updates properly. - await this.onClientRestarted(client) - }), - client.restartedWorker(async (uri) => { - console.log('[InfoProvider] got worker restarted event') - await this.onWorkerRestarted(uri) - }), - client.didSetLanguage(() => this.onLanguageChanged()) - ) - - // Note that when new client is first created it still fires client.restarted - // event, so all onClientRestarted can happen there so we don't do it twice. - } - - async onWorkerRestarted (uri: string): Promise { - await this.infoviewApi?.serverStopped(undefined) // clear any server stopped state - if (this.workersFailed.has(uri)) { - this.workersFailed.delete(uri) - console.log('[InfoProvider] Restarting worker for file: ' + uri) - } - await this.sendPosition() - } - - async onWorkerStopped (uri: string, client: LeanClient, reason: any) { - await this.infoviewApi?.serverStopped(reason) - - if (!this.workersFailed.has(uri)) { - this.workersFailed.set(uri, reason) - } - console.log(`[InfoProvider]client crashed: ${uri}`) - await client.showRestartMessage() - } - - onClientRemoved (client: LeanClient) { - // todo: remove subscriptions for this client... - } - - async onActiveClientStopped (client: LeanClient, activeClient: boolean, reason: any) { - // Will show a message in case the active client stops - // add failed client into a list (will be removed in case the client is restarted) - if (activeClient) { - // means that client and active client are the same and just show the error message - await this.infoviewApi?.serverStopped(reason) - } - - console.log(`[InfoProvider] client stopped`) - - await client.showRestartMessage() - } - - dispose (): void { - // active client is changing. - this.clearNotificationHandlers() - this.clearRpcSessions(null) - for (const s of this.clientSubscriptions) { s.dispose() } - for (const s of this.subscriptions) { s.dispose() } - } - - isOpen (): boolean { - return /* this.webviewPanel?.visible === */ true - } - - async runTestScript (javaScript: string): Promise { - if (this.infoviewApi != null) { - return await this.infoviewApi.runTestScript(javaScript) - } else { - throw new Error('Cannot run test script, infoview is closed.') - } - } - - async getHtmlContents (): Promise { - if (this.infoviewApi != null) { - return await this.infoviewApi.getInfoviewHtml() - } else { - throw new Error('Cannot retrieve infoview HTML, infoview is closed.') - } - } - - async sleep (ms: number) { - return await new Promise((resolve) => setTimeout(resolve, ms)) - } - - async toggleAllMessages (): Promise { - if (this.infoviewApi != null) { - await this.infoviewApi.requestedAction({ kind: 'toggleAllMessages' }) - } - } - - private clearNotificationHandlers () { - for (const [, [, subscriptions]] of this.clientNotifSubscriptions) { for (const h of subscriptions) h.dispose() } - this.clientNotifSubscriptions.clear() - for (const [, [, subscriptions]] of this.serverNotifSubscriptions) { for (const h of subscriptions) h.dispose() } - this.serverNotifSubscriptions.clear() - } - - private clearRpcSessions (client: LeanClient | null) { - const remaining = new Map() - for (const [sessionId, sess] of this.rpcSessions) { - if (client === null || sess.client === client) { - sess.dispose() - } else { - remaining.set(sessionId, sess) - } - } - this.rpcSessions = remaining - } - - getApi () { - return this.editorApi - } - - async openPreview (editor: monaco.editor.IStandaloneCodeEditor, infoviewApi: InfoviewApi) { - this.infoviewApi = infoviewApi - this.editor = editor - await this.initInfoView(editor, this.client!) - } - - private async initInfoView (editor: monaco.editor.IStandaloneCodeEditor | undefined, client: LeanClient | null) { - if (editor != null) { - const loc = this.getLocation(editor) - if (loc != null) { - console.log('initialize infoview api') - await this.infoviewApi?.initialize(loc) - } - } - - // The infoview gets information about file progress, diagnostics, etc. - // by listening to notifications. Send these notifications when the infoview starts - // so that it has up-to-date information. - if ((client?.initializeResult) != null) { - await this.infoviewApi?.serverStopped(undefined) // clear any server stopped state - await this.infoviewApi?.serverRestarted(client.initializeResult) - await this.sendDiagnostics(client) - await this.sendProgress(client) - await this.sendPosition() - await this.sendConfig() - } - } - - private async sendConfig () { - await this.infoviewApi?.changedInfoviewConfig({ - allErrorsOnLine: true, //getInfoViewAllErrorsOnLine(), - autoOpenShowsGoal: true, // getInfoViewAllErrorsOnLine(), - debounceTime: 50, // getInfoViewAutoOpenShowGoal() - - // TODO: I set all of these to false to get things working, - // but what would be correct? - showExpectedType: false, - showGoalNames: false, - emphasizeFirstGoal: false, - reverseTacticState: false, - showTooltipOnHover: false, - }) - } - - private async sendDiagnostics (client: LeanClient) { - if (this.infoviewApi !== undefined) { - client.getDiagnostics()?.forEach(async (uri, diags) => { - const params = client.getDiagnosticParams(uri, diags) - await this.infoviewApi!.gotServerNotification('textDocument/publishDiagnostics', params) - }) - } - } - - private async sendProgress (client: LeanClient) { - if (this.infoviewApi == null) return - for (const [uri, processing] of client.progress) { - const params: LeanFileProgressParams = { - textDocument: { - uri: c2pConverter.asUri(uri), - version: 0 // HACK: The infoview ignores this - }, - processing - } - await this.infoviewApi.gotServerNotification('$/lean/fileProgress', params) - } - } - - private onLanguageChanged () { - this.sendPosition().then(() => this.sendConfig()) - } - - private getLocation (editor: monaco.editor.IStandaloneCodeEditor): ls.Location | undefined { - if (!editor) return undefined - const uri = editor.getModel()?.uri - const selection = editor.getSelection()! - return { - uri: uri!.toString(), - range: toLanguageServerRange(selection) - } - } - - private async sendPosition () { - const editor = this.editor - if (editor == null) return - const loc = this.getLocation(editor) - if (!this.client.running){ - await this.infoviewApi?.serverStopped(undefined) - } else if (this.workersFailed.size > 0) { - const uri = window.activeTextEditor?.document.uri.toString() ?? '' - let reason: any | undefined - if (this.workersFailed.has(uri)) { - reason = this.workersFailed.get(uri) - } - if (reason) { - // send stopped event - await this.infoviewApi?.serverStopped(reason) - } else { - await this.updateStatus(loc) - } - } else { - await this.updateStatus(loc) - } - } - - private async updateStatus (loc: ls.Location | undefined): Promise { - await this.infoviewApi?.changedCursorLocation(loc) - } - - private async revealEditorSelection (uri: Uri, selection?: monaco.Range) { - if (this.editor == null) { - console.error("Editor not set") - return - } - if (selection !== undefined) { - this.editor.revealRange(selection)//TextEditorRevealType.InCenterIfOutsideViewport - this.editor.setSelection(selection) - // ensure the text document has the keyboard focus. - this.editor.focus() - } - } - - private async handleInsertText (text: string, kind: TextInsertKind, uri?: Uri, pos?: monaco.Position) { - if (this.editor == null) { - return - } - pos = (pos != null) ? pos : this.editor.getSelection().getStartPosition() - if (kind === 'above') { - // in this case, assume that we actually want to insert at the same - // indentation level as the neighboring text - const spaces = this.editor.getModel().getLineFirstNonWhitespaceColumn(pos.lineNumber) - 1 - const margin_str = [...Array(spaces).keys()].map(x => ' ').join('') - let new_command = text.replace(/\n/g, '\n' + margin_str) - new_command = `${margin_str}${new_command}\n` - const insertPosition = monaco.Range.fromPositions({lineNumber: pos.lineNumber, column: 0}) - - await this.editor.pushUndoStop() - await this.editor.executeEdits( - "infoview", - [{ range: insertPosition, text: new_command, forceMoveMarkers: true }], - ) - } else { - if (pos != null) { - await this.editor.pushUndoStop() - await this.editor.executeEdits( - "infoview", - [{ range: monaco.Range.fromPositions(pos), text: text, forceMoveMarkers: true }], - ) - } - } - this.editor.focus() - } -} diff --git a/client/src/editor/leanclient.ts b/client/src/editor/leanclient.ts deleted file mode 100644 index 40618101..00000000 --- a/client/src/editor/leanclient.ts +++ /dev/null @@ -1,343 +0,0 @@ -/* This file is based on `vscode-lean4/src/leanclient.ts` */ - -import { - TextDocument, EventEmitter, Diagnostic, - DocumentHighlight, Range, DocumentHighlightKind, - Disposable, Uri, DiagnosticCollection, - WorkspaceFolder, workspace -} from 'vscode' -import { - DidChangeTextDocumentParams, - DidCloseTextDocumentParams, - InitializeResult, - MonacoLanguageClient as LanguageClient, - LanguageClientOptions, - PublishDiagnosticsParams, - CloseAction, ErrorAction, IConnectionProvider, -} from 'monaco-languageclient' -import * as monaco from 'monaco-editor/esm/vs/editor/editor.api.js' -import { State } from 'vscode-languageclient' -import * as ls from 'vscode-languageserver-protocol' - -import { getElaborationDelay } from './config' -import { LeanFileProgressParams, LeanFileProgressProcessingInfo } from '@leanprover/infoview-api' -import { c2pConverter, p2cConverter, patchConverters } from './utils/converters' - -const escapeRegExp = (s: string) => s.replace(/[.*+?^${}()|[\]\\]/g, '\\$&') - -export type ServerProgress = Map - -export function getFullRange (diag: Diagnostic): Range { - return (diag as any)?.fullRange || diag.range -} - -export class LeanClient implements Disposable { - running: boolean = false - private client: LanguageClient | undefined - private noPrompt: boolean = false - - private readonly didChangeEmitter = new EventEmitter() - didChange = this.didChangeEmitter.event - - private readonly diagnosticsEmitter = new EventEmitter() - diagnostics = this.diagnosticsEmitter.event - - private readonly didSetLanguageEmitter = new EventEmitter() - didSetLanguage = this.didSetLanguageEmitter.event - - private readonly didCloseEmitter = new EventEmitter() - didClose = this.didCloseEmitter.event - - private readonly customNotificationEmitter = new EventEmitter<{ method: string, params: any }>() - /** Fires whenever a custom notification (i.e. one not defined in LSP) is received. */ - customNotification = this.customNotificationEmitter.event - - /** saved progress info in case infoview is opened, it needs to get all of it. */ - progress: ServerProgress = new Map() - - private readonly progressChangedEmitter = new EventEmitter<[string, LeanFileProgressProcessingInfo[]]>() - progressChanged = this.progressChangedEmitter.event - - private readonly stoppedEmitter = new EventEmitter() - stopped = this.stoppedEmitter.event - - private readonly restartedEmitter = new EventEmitter() - restarted = this.restartedEmitter.event - - private readonly restartingEmitter = new EventEmitter() - restarting = this.restartingEmitter.event - - private readonly restartedWorkerEmitter = new EventEmitter() - restartedWorker = this.restartedWorkerEmitter.event - - private readonly serverFailedEmitter = new EventEmitter() - serverFailed = this.serverFailedEmitter.event - - constructor ( - private readonly connectionProvider: IConnectionProvider, - public readonly showRestartMessage: () => void, - private readonly initializationOptions = {}) { - - } - - dispose (): void { - if (this.client.isRunning()) { - this.client.dispose() - } else { - this.client.onDidChangeState((ev) => { - if (ev.newState == State.Running) { - setTimeout(() => { // Wait for client to send `initialized` before `shutdown` - this.client.dispose() - }, 0) - } - }) - } - } - - async restart (project): Promise { - const startTime = Date.now() - - if (!project) { - project = 'mathlib-demo' - } - - console.log(`[LeanClient] Restarting Lean Server with project ${project}`) - if (this.isStarted()) { - // TODO: This times out in lean4game... - await this.stop() - } - - this.restartingEmitter.fire(undefined) - - const clientOptions: LanguageClientOptions = { - // use a language id as a document selector - documentSelector: ['lean4'], - workspaceFolder: {uri: "hello"}, - initializationOptions: { - editDelay: getElaborationDelay(), - hasWidgets: true, - ...this.initializationOptions - }, - connectionOptions: { - maxRestartCount: 0, - cancellationStrategy: undefined as any - }, - // disable the default error handler - errorHandler: { - error: () => { this.showRestartMessage(); return { action: ErrorAction.Continue }}, - closed: () => ({ action: CloseAction.DoNotRestart }) - }, - middleware: { - handleDiagnostics: (uri, diagnostics, next) => { - next(uri, diagnostics) - if (this.client == null) return - const uri_ = c2pConverter.asUri(uri) - const diagnostics_ = [] - for (const d of diagnostics) { - const d_: ls.Diagnostic = { - ...c2pConverter.asDiagnostic(d) - } - diagnostics_.push(d_) - } - this.diagnosticsEmitter.fire({ uri: uri_, diagnostics: diagnostics_ }) - }, - - // Closing does not work properly, so we deactivate it here: - didClose: async (data, next) => {}, - - didChange: async (data, next) => { - await next(data) - if (!this.running || (this.client == null)) return // there was a problem starting lean server. - const params = c2pConverter.asChangeTextDocumentParams(data) - this.didChangeEmitter.fire(params) - }, - - provideDocumentHighlights: async (doc, pos, ctok, next) => { - const leanHighlights = await next(doc, pos, ctok) - if (leanHighlights?.length) return leanHighlights - - // vscode doesn't fall back to textual highlights, - // so we need to do that manually - await new Promise((res) => setTimeout(res, 250)) - if (ctok.isCancellationRequested) return - - const wordRange = doc.getWordRangeAtPosition(pos) - if (wordRange == null) return - const word = doc.getText(wordRange) - - const highlights: DocumentHighlight[] = [] - const text = doc.getText() - const nonWordPattern = '[`~@$%^&*()-=+\\[{\\]}⟨⟩⦃⦄⟦⟧⟮⟯‹›\\\\|;:\",./\\s]|^|$' - const regexp = new RegExp(`(?<=${nonWordPattern})${escapeRegExp(word)}(?=${nonWordPattern})`, 'g') - for (const match of text.matchAll(regexp)) { - const start = doc.positionAt(match.index ?? 0) - highlights.push({ - range: new Range(start, start.translate(0, match[0].length)), - kind: DocumentHighlightKind.Text - }) - } - - return highlights - } - } - } - if (!this.client) { - this.client = new LanguageClient({ - id: 'lean4', - name: 'Lean 4', - clientOptions, - connectionProvider: this.connectionProvider - }) - } - - // HACK: Prevent monaco from panicking when the Lean server crashes - this.client.handleFailedRequest = (type, token: any, error: any, defaultValue, showNotification?: boolean) => { - return defaultValue - } - - let insideRestart = true - patchConverters(this.client.protocol2CodeConverter, this.client.code2ProtocolConverter) - try { - this.client.onDidChangeState(async (s) => { - // see https://github.com/microsoft/vscode-languageserver-node/issues/825 - if (s.newState === State.Starting) { - console.log('[LeanClient] starting') - } else if (s.newState === State.Running) { - const end = Date.now() - console.log(`[LeanClient] running, started in ${end - startTime} ms`) - this.running = true // may have been auto restarted after it failed. - if (!insideRestart) { - this.restartedEmitter.fire() - } - } else if (s.newState === State.Stopped) { - this.running = false - console.log('[LeanClient] has stopped or it failed to start') - if (!this.noPrompt) { - // only raise this event and show the message if we are not the ones - // who called the stop() method. - this.stoppedEmitter.fire({ message: 'Lean server has stopped.', reason: '' }) - } - } - }) - await this.client.start() - this.running = true - } catch (error) { - console.log(error) - this.serverFailedEmitter.fire('' + error) - insideRestart = false - return - } - - // HACK(WN): Register a default notification handler to fire on custom notifications. - // A mechanism to do this is provided in vscode-jsonrpc. One can register a `StarNotificationHandler` - // here: https://github.com/microsoft/vscode-languageserver-node/blob/b2fc85d28a1a44c22896559ee5f4d3ba37a02ef5/jsonrpc/src/common/connection.ts#L497 - // which fires on any LSP notifications not in the standard, for example the `$/lean/..` ones. - // However this mechanism is not exposed in vscode-languageclient, so we hack around its implementation. - const starHandler = (method: string, params_: any) => { - if (method === '$/lean/fileProgress' && (this.client != null)) { - const params = params_ as LeanFileProgressParams - const uri = p2cConverter.asUri(params.textDocument.uri) - this.progressChangedEmitter.fire([uri.toString(), params.processing]) - // save the latest progress on this Uri in case infoview needs it later. - this.progress.set(uri, params.processing) - } - - this.customNotificationEmitter.fire({ method, params: params_ }) - } - // eslint-disable-next-line @typescript-eslint/no-unsafe-argument - this.client.onNotification(starHandler as any, () => {}) - - this.restartedEmitter.fire({project: project}) - insideRestart = false - } - - // async start (project): Promise { - // return await this.restart(project) - // } - - isStarted (): boolean { - return this.client !== undefined - } - - isRunning (): boolean { - if (this.client != null) { - return this.running - } - return false - } - - async stop (): Promise { - // assert(() => this.isStarted()) - if ((this.client != null) && this.running) { - this.noPrompt = true - try { - // some timing conditions can happen while running unit tests that cause - // this to throw an exception which then causes those tests to fail. - await this.client.stop() - } catch (e) { - console.log(`[LeanClient] Error stopping language client: ${e}`) - } - } - - this.noPrompt = false - this.progress = new Map() - this.client = undefined - this.running = false - } - - async restartFile (doc: TextDocument): Promise { - if (!this.running) return // there was a problem starting lean server. - - const uri = doc.uri.toString() - console.log(`[LeanClient] Restarting File: ${uri}`) - // This causes a text document version number discontinuity. In - // (didChange (oldVersion) => restartFile => didChange (newVersion)) - // the client emits newVersion = oldVersion + 1, despite the fact that the - // didOpen packet emitted below initializes the version number to be 1. - // This is not a problem though, since both client and server are fine - // as long as the version numbers are monotonous. - void this.client?.sendNotification('textDocument/didClose', { - textDocument: { - uri - } - }) - void this.client?.sendNotification('textDocument/didOpen', { - textDocument: { - uri, - languageId: 'lean4', - version: 1, - text: doc.getText() - } - }) - this.restartedWorkerEmitter.fire(uri) - } - - // eslint-disable-next-line @typescript-eslint/explicit-module-boundary-types - async sendRequest (method: string, params: any): Promise { - return this.running && (this.client != null) - ? await this.client.sendRequest(method, params) - : await new Promise((_, reject) => { reject('Client is not running') }) - } - - // eslint-disable-next-line @typescript-eslint/explicit-module-boundary-types - sendNotification (method: string, params: any): Promise | undefined { - return this.running && (this.client != null) ? this.client.sendNotification(method, params) : undefined - } - - async getDiagnosticParams (uri: Uri, diagnostics: readonly Diagnostic[]): Promise { - const params: PublishDiagnosticsParams = { - uri: c2pConverter.asUri(uri), - diagnostics: await c2pConverter.asDiagnostics(diagnostics as Diagnostic[]) - } - return params - } - - getDiagnostics (): DiagnosticCollection | undefined { - return this.running ? this.client?.diagnostics : undefined - } - - get initializeResult (): InitializeResult | undefined { - return this.running ? this.client?.initializeResult : undefined - } - -} diff --git a/client/src/editor/taskgutter.ts b/client/src/editor/taskgutter.ts deleted file mode 100644 index 0490eb3d..00000000 --- a/client/src/editor/taskgutter.ts +++ /dev/null @@ -1,119 +0,0 @@ -/* This file is based on `vscode-lean4/src/taskgutter.ts` */ - -import * as monaco from 'monaco-editor/esm/vs/editor/editor.api.js' -import { LeanFileProgressKind, LeanFileProgressProcessingInfo } from '@leanprover/infoview-api'; -import { LeanClient } from './leanclient'; -import { fromLanguageServerRange } from './utils/converters'; - -class LeanFileTaskGutter { - private timeout?: NodeJS.Timeout - private decoIds: string[] = [] - - constructor(private editor: monaco.editor.IStandaloneCodeEditor, private decorations: Map, private processed: LeanFileProgressProcessingInfo[]) { - this.schedule(100) - } - - setProcessed(processed: LeanFileProgressProcessingInfo[]) { - if (processed === this.processed) return; - const oldProcessed = this.processed; - this.processed = processed; - if (processed === undefined) { - this.processed = [] - this.clearTimeout(); - this.updateDecos(); - } else if (this.timeout === undefined) { - this.schedule(oldProcessed === undefined ? 500 : 20) - } - } - - private schedule(ms: number) { - this.timeout = setTimeout(() => { - this.timeout = undefined - this.updateDecos() - }, ms) - } - - private clearTimeout() { - if (this.timeout !== undefined) { - clearTimeout(this.timeout) - this.timeout = undefined; - } - } - - private updateDecos() { - this.decoIds = this.editor.getModel().deltaDecorations(this.decoIds, - this.processed - .map(info => ({ - options: this.decorations.get(info.kind === undefined ? LeanFileProgressKind.Processing : info.kind), - range : fromLanguageServerRange(info.range) - })) - ) - } - - dispose() { - this.clearTimeout(); - } -} - -export class LeanTaskGutter { - private decorations: Map = - new Map(); - private status: { [uri: string]: LeanFileProgressProcessingInfo[] } = {}; - private gutters: { [uri: string]: LeanFileTaskGutter | undefined } = {}; - private subscriptions: any[] = []; - - constructor(private client: LeanClient, private editor: monaco.editor.IStandaloneCodeEditor) { - this.decorations.set(LeanFileProgressKind.Processing, - { - overviewRuler: { - position: monaco.editor.OverviewRulerLane.Left, - color: 'rgba(255, 165, 0, 0.5)', - }, - glyphMarginClassName: 'processing', - hoverMessage: {value: 'busily processing...'} - }) - this.decorations.set(LeanFileProgressKind.FatalError, - { - overviewRuler: { - position: monaco.editor.OverviewRulerLane.Left, - color: 'rgba(255, 0, 0, 0.5)', - }, - glyphMarginClassName: 'glyph-margin-error', - hoverMessage: {value: 'processing stopped'} - }, - ) - - this.subscriptions.push( - client.progressChanged(([uri, processing]) => { - this.status[uri.toString()] = processing - this.updateDecos() - })); - } - - private updateDecos() { - const uris: { [uri: string]: boolean } = {} - // for (const editor of window.visibleTextEditors) { - const uri = this.editor.getModel().uri.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(this.editor, this.decorations, processed) - } - // } - for (const uri of Object.getOwnPropertyNames(this.gutters)) { - if (!uris[uri]) { - this.gutters[uri]?.dispose(); - this.gutters[uri] = undefined; - // TODO: also clear this.status for this uri ? - } - } - } - - dispose(): void { - // for (const decoration of this.decorations.values()) { decoration.dispose() } - for (const s of this.subscriptions) { s.dispose(); } - } -} diff --git a/client/src/editor/utils/converters.ts b/client/src/editor/utils/converters.ts deleted file mode 100644 index ab4cce07..00000000 --- a/client/src/editor/utils/converters.ts +++ /dev/null @@ -1,76 +0,0 @@ -/* This file is based on `vscode-lean4/src/utils/converters.ts` */ - -/** - * For LSP communication, we need a way to translate between LSP types and corresponding VSCode types. - * By default this translation is provided as a bunch of methods on a `LanguageClient`, but this is - * awkward to use in multi-client workspaces wherein we need to look up specific clients. In fact the - * conversions are *not* stateful, so having them depend on the client is unnecessary. Instead, we - * provide global converters here. - * - * Some of the conversions are patched to support extended Lean-specific structures. - * - * @module - */ - -import { createConverter as createP2CConverter } from 'vscode-languageclient/lib/common/protocolConverter' -import { createConverter as createC2PConverter } from 'vscode-languageclient/lib/common/codeConverter' -import * as ls from 'vscode-languageserver-protocol' -import * as code from 'vscode' -import { Code2ProtocolConverter, Protocol2CodeConverter } from 'vscode-languageclient' -import { MonacoLanguageClient} from 'monaco-languageclient/.' -import * as monaco from 'monaco-editor/esm/vs/editor/editor.api.js' - -interface Lean4Diagnostic extends ls.Diagnostic { - fullRange: ls.Range -} - -export const p2cConverter = createP2CConverter(undefined, true, true) -export const c2pConverter = createC2PConverter(undefined) - -export function patchConverters (p2cConverter: Protocol2CodeConverter, c2pConverter: Code2ProtocolConverter) { - // eslint-disable-next-line @typescript-eslint/unbound-method - const oldAsDiagnostic = p2cConverter.asDiagnostic - p2cConverter.asDiagnostic = function (protDiag: Lean4Diagnostic): code.Diagnostic { - if (!protDiag.message) { - // Fixes: Notification handler 'textDocument/publishDiagnostics' failed with message: message must be set - protDiag.message = ' ' - } - const diag = oldAsDiagnostic.apply(this, [protDiag]) - // diag.fullRange = p2cConverter.asRange(protDiag.fullRange) - return diag - } - p2cConverter.asDiagnostics = async (diags) => diags.map(d => p2cConverter.asDiagnostic(d)) - - // eslint-disable-next-line @typescript-eslint/unbound-method - const c2pAsDiagnostic = c2pConverter.asDiagnostic - c2pConverter.asDiagnostic = function (diag: code.Diagnostic & { fullRange: code.Range }): Lean4Diagnostic { - const protDiag = c2pAsDiagnostic.apply(this, [diag]) - return { ...protDiag, fullRange: c2pConverter.asRange(diag.fullRange) } - } - c2pConverter.asDiagnostics = async (diags) => diags.map(d => c2pConverter.asDiagnostic(d)) -} - -patchConverters(p2cConverter, c2pConverter) - -export function toLanguageServerRange (range: monaco.Range): ls.Range { - return { - start: { line: range.startLineNumber - 1, character: range.startColumn - 1}, - end: { line: range.endLineNumber - 1, character: range.endColumn - 1} - } -} - -export function fromLanguageServerPosition (pos: ls.Position): monaco.Position { - return new monaco.Position( - pos.line + 1, - pos.character + 1 - ) -} - -export function fromLanguageServerRange (range: ls.Range): monaco.Range { - return new monaco.Range( - range.start.line + 1, - range.start.character + 1, - range.end.line + 1, - range.end.character + 1 - ) -} diff --git a/client/src/monacoSetup.ts b/client/src/monacoSetup.ts index 493b9d4d..4dc13434 100644 --- a/client/src/monacoSetup.ts +++ b/client/src/monacoSetup.ts @@ -3,7 +3,7 @@ import { wireTmGrammars } from 'monaco-editor-textmate' import * as leanSyntax from './syntaxes/lean.json' import * as leanMarkdownSyntax from './syntaxes/lean-markdown.json' import * as codeblockSyntax from './syntaxes/codeblock.json' -import languageConfig from '../vscode-lean4/vscode-lean4/language-configuration.json'; +import languageConfig from '../monaco-lean4/vscode-lean4/language-configuration.json'; import { loadWASM } from 'onigasm' import * as monaco from 'monaco-editor/esm/vs/editor/editor.api.js' import { MonacoServices } from 'monaco-languageclient'; diff --git a/client/vscode-lean4 b/client/vscode-lean4 deleted file mode 160000 index a4d92e5c..00000000 --- a/client/vscode-lean4 +++ /dev/null @@ -1 +0,0 @@ -Subproject commit a4d92e5c9354bfe4a92d915208137a5e98d43689