diff --git a/editor/src/index.ts b/editor/src/index.ts index c4bd0abe..6a568a8f 100644 --- a/editor/src/index.ts +++ b/editor/src/index.ts @@ -1,4 +1,5 @@ import { FileFormat, Message, MessageType } from "../../shared"; +import { getSemanticColors } from "./semanticColors"; import { defaultToMarkdown, markdown, ThemeStyle, WaterproofEditor, WaterproofEditorConfig } from "@impermeable/waterproof-editor"; // TODO: The tactics completions are static, we want them to be dynamic (LSP supplied and/or configurable when the editor is running) import waterproofTactics from "../../completions/tactics.json"; @@ -73,8 +74,6 @@ function createConfiguration(format: FileFormat, codeAPI: VSCodeAPI) { tagConfiguration: tagConfigurationLean, serializer: new LeanSerializer(), languageConfig: { - highlightDark: langVerbose.highlight_dark, - highlightLight: langVerbose.highlight_light, languageSupport: langVerbose.verbose(), }, } @@ -147,6 +146,10 @@ window.onload = () => { default: throw Error("Invalid theme encountered"); } })(); + for (const [key, value] of Object.entries(getSemanticColors(themeStyle))) { + document.documentElement.style.setProperty(key, value); + } + const editor = new WaterproofEditor(editorElement, cfg, themeStyle); //@ts-expect-error For now, expose editor in the window. Allows for calling editorInstance methods via the debug console. @@ -237,8 +240,15 @@ window.onload = () => { } break; } - case MessageType.themeUpdate: + case MessageType.themeUpdate: { editor.updateNodeViewThemes(msg.body.theme); + for (const [key, value] of Object.entries(getSemanticColors(msg.body.theme))) { + document.documentElement.style.setProperty(key, value); + } + break; + } + case MessageType.semanticTokens: + editor.setSemanticTokens(msg.body.tokens); break; default: // If we reach this 'default' case, then we have encountered an unknown message type. diff --git a/editor/src/semanticColors.ts b/editor/src/semanticColors.ts new file mode 100644 index 00000000..5c916bb5 --- /dev/null +++ b/editor/src/semanticColors.ts @@ -0,0 +1,29 @@ +import { ThemeStyle } from "@impermeable/waterproof-editor"; + +export type SemanticColorMap = Record; + +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; +} diff --git a/editor/src/vscodemapping.css b/editor/src/vscodemapping.css index 2704c928..d4ae24ad 100644 --- a/editor/src/vscodemapping.css +++ b/editor/src/vscodemapping.css @@ -42,9 +42,6 @@ --wp-notificationsForeground: var(--vscode-notifications-foreground); --wp-quickInputBackground: var(--vscode-quickInput-background); --wp-quickInputForeground: var(--vscode-quickInput-foreground); - --wp-terminalAnsiGreen: var(--vscode-terminal-ansiGreen); - --wp-terminalAnsiRed: var(--vscode-terminal-ansiRed); - --wp-terminalAnsiYellow: var(--vscode-terminal-ansiYellow); --wp-textCodeBlockBackground: var(--vscode-textCodeBlock-background); --wp-textSeparatorForeground: var(--vscode-textSeparator-foreground); -} \ No newline at end of file +} diff --git a/shared/Messages.ts b/shared/Messages.ts index 90d475f2..e5358e2a 100644 --- a/shared/Messages.ts +++ b/shared/Messages.ts @@ -1,4 +1,4 @@ -import { DocChange, WrappingDocChange, InputAreaStatus, HistoryChange, ThemeStyle, OffsetDiagnostic } from "@impermeable/waterproof-editor"; +import { DocChange, WrappingDocChange, InputAreaStatus, HistoryChange, ThemeStyle, OffsetDiagnostic, OffsetSemanticToken } from "@impermeable/waterproof-editor"; import { RocqGoalAnswer, HypVisibility, PpString } from "../lib/types"; import { Completion } from "@impermeable/waterproof-editor"; import { ServerStatus } from "./ServerStatus"; @@ -53,6 +53,7 @@ export type Message = // The payload is forwarded to an InfoView instance, so its type does not concern us // eslint-disable-next-line @typescript-eslint/no-explicit-any | MessageBase + | MessageBase }> ; /** @@ -87,5 +88,6 @@ export const enum MessageType { teacher, themeUpdate, viewportHint, - infoviewRpc + infoviewRpc, + semanticTokens } diff --git a/src/lsp-client/lean/client.ts b/src/lsp-client/lean/client.ts index 79fe2c0c..e13f9ad9 100644 --- a/src/lsp-client/lean/client.ts +++ b/src/lsp-client/lean/client.ts @@ -1,6 +1,6 @@ import { LeanGoalAnswer, LeanGoalRequest } from "../../../lib/types"; import { LspClient } from "../client"; -import { EventEmitter, Position, TextDocument, Disposable, Range, OutputChannel, Diagnostic, DiagnosticSeverity } from "vscode"; +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"; @@ -8,19 +8,21 @@ import { WaterproofConfigHelper, WaterproofLogger as wpl, WaterproofSetting } fr import { LanguageClientProvider, WpDiagnostic } from "../clientTypes"; import { WebviewManager } from "../../webviewManager"; import { findOccurrences } from "../qedStatus"; -import { InputAreaStatus } from "@impermeable/waterproof-editor"; +import { InputAreaStatus, OffsetSemanticToken, SemanticTokenType } from "@impermeable/waterproof-editor"; import { ServerStoppedReason } from "@leanprover/infoview-api"; -import { DidChangeTextDocumentParams, DidCloseTextDocumentParams } from "vscode-languageclient"; +import { DidChangeTextDocumentParams, DidCloseTextDocumentParams, SemanticTokensRegistrationType } from "vscode-languageclient"; import { FileProgressKind, MessageType } from "../../../shared"; export class LeanLspClient extends LspClient { 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; + private isBusy: boolean = true; constructor(clientProvider: LanguageClientProvider, channel: OutputChannel) { super(clientProvider, channel); @@ -80,12 +82,15 @@ export class LeanLspClient extends LspClient { } 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 { 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 { public clientStopped = this.clientStoppedEmitter.event; async dispose(timeout?: number): Promise { + 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 { + 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 = 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}, + }); + } + + 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; + } + } + protected onDocumentChanged(): void { this.isBusy = true; } -} \ No newline at end of file +}