Lean lsp highlighting by Tammo0987 · Pull Request #330 · impermeable/waterproof-vscode

Tammo0987 · 2026-03-24T17:04:24Z

Description

Implements the basics of semantic highlighting and removes static syntax highlighting for lean.

Testing this PR

Use the waterproof-genre repository to test it. But currently a specific version is required.

Related to: impermeable/waterproof-editor#83

Copilot

Pull request overview

This PR adds basic Lean semantic highlighting by forwarding LSP semantic tokens to the Waterproof editor webview, and removes the previous static (syntax) highlighting configuration for Lean.

Changes:

Request and forward LSP semantic tokens from the Lean LSP client to the webview (debounced on file progress).
Add a new semanticTokens webview message and wire the editor to apply tokens + set theme-dependent semantic token colors via CSS variables.
Remove Lean’s static highlight config and clean up unused CSS mappings.

Reviewed changes

Copilot reviewed 5 out of 5 changed files in this pull request and generated 4 comments.

Show a summary per file

File	Description
`src/lsp-client/lean/client.ts`	Requests semantic tokens from the VS Code semantic token provider and forwards them to the webview.
`shared/Messages.ts`	Adds a new `MessageType.semanticTokens` message shape for token forwarding.
`editor/src/index.ts`	Applies semantic token CSS vars on theme changes and forwards semantic tokens into the editor instance.
`editor/src/semanticColors.ts`	Introduces theme-dependent CSS variable values for semantic token coloring.
`editor/src/vscodemapping.css`	Removes terminal ANSI color mappings (no longer used).
`.zed/settings.json`	Adds Zed editor settings file to the repo.

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

Copilot · 2026-03-24T17:09:48Z

src/lsp-client/lean/client.ts

+    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},
+        });


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).

Should be very rare in practice and will recover on the next request, I think its not worth adding that.

src/lsp-client/lean/client.ts

Copilot · 2026-03-24T17:09:49Z

shared/Messages.ts

    // 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<MessageType.infoviewRpc, { payload: any }>
+    | MessageBase<MessageType.semanticTokens, { tokens: Array<OffsetSemanticToken> }>


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.

Suggested change

| MessageBase<MessageType.semanticTokens, { tokens: Array<OffsetSemanticToken> }>

| MessageBase<MessageType.semanticTokens, { tokens: Array<OffsetSemanticToken>, version: number }>

Should be very rare in practice and will recover on the next request, I think its not worth adding that.

Copilot · 2026-03-24T17:09:50Z

src/lsp-client/lean/client.ts

+    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;
+        }
+    }


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.

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.

Tammo0987 added 11 commits February 24, 2026 16:29

wired lean lsp tokens into the editor for semantic code highlighting

55834cf

Merge branch 'mapping' into lean-lsp-highlighting

df64279

fixes error after merge

79f97d0

fix token mapping

fd82325

add colors for theme

3ec5ae4

Merge branch 'mapping' into lean-lsp-highlighting

cad7d8b

adds semantic highlighting colors (draft)

4bb9695

remove static highlighting for lean

9a29beb

change var color

7123076

remove todo

fbd18c1

minorfixes

7a79209

Copilot AI review requested due to automatic review settings March 24, 2026 17:04

Tammo0987 mentioned this pull request Mar 24, 2026

Lean lsp highlighting impermeable/waterproof-editor#83

Open

Copilot started reviewing on behalf of Tammo0987 March 24, 2026 17:04 View session

remove zed settings file

03e078a

Copilot AI reviewed Mar 24, 2026

View reviewed changes

minor fix for debouncing

10d2e75

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Lean lsp highlighting#330

Lean lsp highlighting#330
Tammo0987 wants to merge 13 commits intomappingfrom
lean-lsp-highlighting

Tammo0987 commented Mar 24, 2026 •

edited

Loading

Uh oh!

Copilot AI left a comment

Uh oh!

Copilot AI Mar 24, 2026

Uh oh!

Tammo0987 Mar 24, 2026

Uh oh!

Uh oh!

Copilot AI Mar 24, 2026

Uh oh!

Tammo0987 Mar 24, 2026

Uh oh!

Copilot AI Mar 24, 2026

Uh oh!

Tammo0987 Mar 24, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

	\| MessageBase<MessageType.semanticTokens, { tokens: Array<OffsetSemanticToken> }>
	\| MessageBase<MessageType.semanticTokens, { tokens: Array<OffsetSemanticToken>, version: number }>

Conversation

Tammo0987 commented Mar 24, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Description

Testing this PR

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Reviewed changes

Uh oh!

Copilot AI Mar 24, 2026

Choose a reason for hiding this comment

Uh oh!

Tammo0987 Mar 24, 2026

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Copilot AI Mar 24, 2026

Choose a reason for hiding this comment

Uh oh!

Tammo0987 Mar 24, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Mar 24, 2026

Choose a reason for hiding this comment

Uh oh!

Tammo0987 Mar 24, 2026

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Tammo0987 commented Mar 24, 2026 •

edited

Loading