Lean lsp highlighting #330
There are no files selected for viewing
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,29 @@ | ||
| import { ThemeStyle } from "@impermeable/waterproof-editor"; | ||
|
|
||
| export type SemanticColorMap = Record<string, string>; | ||
|
|
||
| const darkColors: SemanticColorMap = { | ||
| "--wp-semanticKeyword": "#7aa2f7", | ||
| "--wp-semanticFunction": "#e0af68", | ||
| "--wp-semanticType": "#2ac3de", | ||
| "--wp-semanticVariable": "#e8c574", | ||
| "--wp-semanticProperty": "#73daca", | ||
| "--wp-semanticLiteral": "#9ece6a", | ||
| "--wp-semanticComment": "#565f89", | ||
| "--wp-semanticLeanSorryLike": "#f7768e", | ||
| }; | ||
|
|
||
| const lightColors: SemanticColorMap = { | ||
| "--wp-semanticKeyword": "#0033b3", | ||
| "--wp-semanticFunction": "#795e26", | ||
| "--wp-semanticType": "#267f99", | ||
| "--wp-semanticVariable": "#9b6800", | ||
| "--wp-semanticProperty": "#0070c1", | ||
| "--wp-semanticLiteral": "#098658", | ||
| "--wp-semanticComment": "#6a9955", | ||
| "--wp-semanticLeanSorryLike": "#cd3131", | ||
| }; | ||
|
|
||
| export function getSemanticColors(theme: ThemeStyle): SemanticColorMap { | ||
| return theme === ThemeStyle.Dark ? darkColors : lightColors; | ||
| } |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,26 +1,28 @@ | ||
| import { LeanGoalAnswer, LeanGoalRequest } from "../../../lib/types"; | ||
| import { LspClient } from "../client"; | ||
| import { CancellationTokenSource, EventEmitter, Position, TextDocument, Disposable, Range, OutputChannel, Diagnostic, DiagnosticSeverity} from "vscode"; | ||
| import { VersionedTextDocumentIdentifier } from "vscode-languageserver-types"; | ||
| import { FileProgressParams } from "../requestTypes"; | ||
| import { leanFileProgressNotificationType, leanGoalRequestType, LeanPublishDiagnosticsParams } from "./requestTypes"; | ||
| import { WaterproofConfigHelper, WaterproofLogger as wpl, WaterproofSetting } from "../../helpers"; | ||
| import { LanguageClientProvider, WpDiagnostic } from "../clientTypes"; | ||
| import { WebviewManager } from "../../webviewManager"; | ||
| import { findOccurrences } from "../qedStatus"; | ||
| import { InputAreaStatus, OffsetSemanticToken, SemanticTokenType } from "@impermeable/waterproof-editor"; | ||
| import { ServerStoppedReason } from "@leanprover/infoview-api"; | ||
| import { DidChangeTextDocumentParams, DidCloseTextDocumentParams, SemanticTokensRegistrationType } from "vscode-languageclient"; | ||
| import { FileProgressKind, MessageType } from "../../../shared"; | ||
|
|
||
| export class LeanLspClient extends LspClient<LeanGoalRequest, LeanGoalAnswer> { | ||
| language = "lean4"; | ||
|
|
||
| private semanticTokenTimer?: NodeJS.Timeout | number; | ||
|
|
||
| /** | ||
| * Whether the Lean server is still processing the document. | ||
| * Used to avoid marking a proof as complete before checking has finished. | ||
| */ | ||
| private isBusy: boolean = true; | ||
|
|
||
| constructor(clientProvider: LanguageClientProvider, channel: OutputChannel) { | ||
| super(clientProvider, channel); | ||
|
|
@@ -80,12 +82,15 @@ export class LeanLspClient extends LspClient<LeanGoalRequest, LeanGoalAnswer> { | |
| } | ||
|
|
||
| protected async onFileProgress(progress: FileProgressParams) { | ||
| if (this.activeDocument?.uri.toString() === progress.textDocument.uri) { | ||
| this.requestSemanticTokensDebounced(this.activeDocument); | ||
| } | ||
|
|
||
| // Call super first so LSP ranges are converted to VSCode Ranges before we store/use them. | ||
| super.onFileProgress(progress); | ||
|
|
||
| if (this.activeDocument?.uri.toString() === progress.textDocument.uri) { | ||
|
|
||
| // --- busy-indicator (Lean edition) --- | ||
| // Find the first processing range, where we want to add the busy-indicator to. | ||
| const firstProcessing = progress.processing.find( | ||
|
|
@@ -193,16 +198,16 @@ export class LeanLspClient extends LspClient<LeanGoalRequest, LeanGoalAnswer> { | |
| if (hasErrorDiagnostic) { | ||
| return InputAreaStatus.Incorrect; | ||
| } | ||
|
|
||
| const goalsPosition = inputArea.end.translate(0, 0); | ||
|
|
||
| const goalsParams = this.createGoalsRequestParameters(document, goalsPosition); | ||
| const response = await this.requestGoals(goalsParams); | ||
|
|
||
| if (!response) { | ||
| return InputAreaStatus.Incorrect; | ||
| } | ||
|
|
||
| const status = response.goals.length > 0 ? InputAreaStatus.Incorrect : InputAreaStatus.Correct; | ||
| return status; | ||
| } | ||
|
|
@@ -236,11 +241,119 @@ export class LeanLspClient extends LspClient<LeanGoalRequest, LeanGoalAnswer> { | |
| public clientStopped = this.clientStoppedEmitter.event; | ||
|
|
||
| async dispose(timeout?: number): Promise<void> { | ||
| if (this.semanticTokenTimer) { | ||
| clearTimeout(this.semanticTokenTimer); | ||
| } | ||
| await super.dispose(timeout); | ||
| this.clientStoppedEmitter.fire({message: 'Lean server has stopped', reason: ''}); | ||
| } | ||
|
|
||
| private requestSemanticTokensDebounced(document: TextDocument) { | ||
| if (this.semanticTokenTimer) { | ||
| clearTimeout(this.semanticTokenTimer); | ||
| } | ||
| this.semanticTokenTimer = setTimeout(() => { | ||
| this.requestAndForwardSemanticTokens(document).catch(err => { | ||
| wpl.debug(`Semantic token request failed: ${err}`) | ||
| }); | ||
| }, 300); | ||
| } | ||
|
|
||
| private async requestAndForwardSemanticTokens(document: TextDocument): Promise<void> { | ||
| if (!this.client.isRunning() || !this.webviewManager) return; | ||
|
|
||
| const feature = this.client.getFeature(SemanticTokensRegistrationType.method); | ||
| if (!feature) return; | ||
|
|
||
| const provider = feature.getProvider(document); | ||
| if (!provider?.full) return; | ||
|
|
||
| const cts = new CancellationTokenSource(); | ||
| const tokens = await Promise.resolve( | ||
| provider.full.provideDocumentSemanticTokens(document, cts.token) | ||
| ).catch(() => undefined).finally(() => cts.dispose()); | ||
|
|
||
| if (!tokens?.data?.length) return; | ||
|
|
||
| const tokenLegend = this.client.initializeResult?.capabilities.semanticTokensProvider?.legend; | ||
| if (!tokenLegend) return; | ||
|
|
||
| const offsetTokens: Array<OffsetSemanticToken> = LeanLspClient.decodeLspTokens(tokens.data).flatMap(t => { | ||
| const tokenType = LeanLspClient.mapLspTokenType(tokenLegend.tokenTypes[t.tokenTypeIndex]); | ||
| if (tokenType === undefined) return []; | ||
|
|
||
| const startOffset = document.offsetAt(new Position(t.line, t.char)); | ||
| return [{ | ||
| startOffset, | ||
| endOffset: startOffset + t.length, | ||
| type: tokenType, | ||
| }]; | ||
| }); | ||
|
|
||
| this.webviewManager.postMessage(document.uri.toString(), { | ||
| type: MessageType.semanticTokens, | ||
| body: {tokens: offsetTokens}, | ||
| }); | ||
|
Comment on lines
+251
to
+296
There was a problem hiding this comment. Semantic token requests can overlap (debounce timer + async provider call), and results may arrive out-of-order; the last-resolving request will overwrite highlights even if it corresponds to an older document version. Consider tracking a monotonically increasing request generation / document.version and discarding stale results (and/or reusing a single CancellationTokenSource that you cancel when scheduling a new request).
Author
There was a problem hiding this comment. Should be very rare in practice and will recover on the next request, I think its not worth adding that. |
||
| } | ||
|
|
||
| private static decodeLspTokens(data: Uint32Array): Array<{ line: number; char: number; length: number; tokenTypeIndex: number }> { | ||
| if (data.length % 5 !== 0) { | ||
| wpl.debug(`[SemanticTokens] Malformed token data: length ${data.length} is not a multiple of 5`); | ||
| } | ||
| const tokens = []; | ||
| let line = 0; | ||
| let char = 0; | ||
| for (let i = 0; i + 4 < data.length; i += 5) { | ||
| const deltaLine = data[i]; | ||
| const deltaStartChar = data[i + 1]; | ||
| if (deltaLine > 0) { | ||
| line += deltaLine; | ||
| char = deltaStartChar; | ||
| } else { | ||
| char += deltaStartChar; | ||
| } | ||
| tokens.push({ | ||
| line, | ||
| char, | ||
| length: data[i + 2], | ||
| tokenTypeIndex: data[i + 3], | ||
| // data[i + 4] is tokenModifiers (unused) | ||
| }); | ||
| } | ||
| return tokens; | ||
| } | ||
|
|
||
| private static mapLspTokenType(lspType: string): SemanticTokenType | undefined { | ||
| switch (lspType) { | ||
| case "keyword": return SemanticTokenType.Keyword; | ||
| case "variable": return SemanticTokenType.Variable; | ||
| case "property": return SemanticTokenType.Property; | ||
| case "function": return SemanticTokenType.Function; | ||
| case "namespace": return SemanticTokenType.Namespace; | ||
| case "type": return SemanticTokenType.Type; | ||
| case "class": return SemanticTokenType.Class; | ||
| case "enum": return SemanticTokenType.Enum; | ||
| case "interface": return SemanticTokenType.Interface; | ||
| case "struct": return SemanticTokenType.Struct; | ||
| case "typeParameter": return SemanticTokenType.TypeParameter; | ||
| case "parameter": return SemanticTokenType.Parameter; | ||
| case "enumMember": return SemanticTokenType.EnumMember; | ||
| case "event": return SemanticTokenType.Event; | ||
| case "method": return SemanticTokenType.Method; | ||
| case "macro": return SemanticTokenType.Macro; | ||
| case "modifier": return SemanticTokenType.Modifier; | ||
| case "comment": return SemanticTokenType.Comment; | ||
| case "string": return SemanticTokenType.String; | ||
| case "number": return SemanticTokenType.Number; | ||
| case "regexp": return SemanticTokenType.Regexp; | ||
| case "operator": return SemanticTokenType.Operator; | ||
| case "decorator": return SemanticTokenType.Decorator; | ||
| case "leanSorryLike": return SemanticTokenType.LeanSorryLike; | ||
| default: return undefined; | ||
| } | ||
| } | ||
|
Comment on lines
+299
to
+354
There was a problem hiding this comment. New semantic-token decoding/mapping logic is non-trivial and currently untested. There are already Jest tests for LeanLspClient in tests/lsp-client/lean; consider adding focused unit tests for decodeLspTokens (delta encoding) and mapLspTokenType to prevent regressions.
Author
There was a problem hiding this comment. I think its not worth it to test it, because the decoding is based on the specification of the lsp and the mapping function is trivial. |
||
|
|
||
| protected onDocumentChanged(): void { | ||
| this.isBusy = true; | ||
| } | ||
| } | ||
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The semanticTokens message payload does not include a document version, unlike diagnostics/init which are versioned. Because semantic token computation is async, the webview can receive stale tokens after newer edits. Consider adding a version field (e.g., document.version) and having the editor ignore tokens that don't match the current document version.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Should be very rare in practice and will recover on the next request, I think its not worth adding that.