diff --git a/CHANGELOG.md b/CHANGELOG.md index 2fca12b98..569c22834 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -4,6 +4,7 @@ - Read "lean-toolchain" files and do not set --default-toolchain to something specific. - elan should not install multiple toolchains. +- Occurrence highlighting can be configured to ignore string matches and use only Lean's LSP responses ### 0.0.40 (Oct 21, 2021): c387eab150b988a47956192b0fc48e950f6c1fca diff --git a/README.md b/README.md index d4c7dc22e..022f334e6 100644 --- a/README.md +++ b/README.md @@ -191,6 +191,8 @@ name of the relative path to the store the logs. * `lean4.typesInCompletionList`: controls whether the types of all items in the list of completions are displayed. By default, only the type of the highlighted item is shown. +* `lean4.editor.occurrenceHighlightWithStringFallback`: controls whether the editor should fall back to string-based occurrence highlighting when there are no symbol occurrences found. + ### Infoview settings * `lean4.infoview.autoOpen`: controls whether the Infoview is automatically displayed when the Lean extension is activated for the first time in a given VS Code workspace(`true` by default). If you manually close the Infoview it will stay closed for that workspace until. You can then open it again using the Ctrl+Shift+P `Lean 4: Infoview: Display Goal` command. diff --git a/vscode-lean4/package.json b/vscode-lean4/package.json index 09d18dfd2..5ea3d1652 100644 --- a/vscode-lean4/package.json +++ b/vscode-lean4/package.json @@ -64,6 +64,11 @@ "default": true, "markdownDescription": "Enable eager replacement of abbreviations that uniquely identify a symbol." }, + "lean4.editor.occurrenceHighlightWithStringFallback": { + "type": "boolean", + "description": "Fall back to string occurrence matching when there are no symbol occurrences from Lean to highlight.", + "default": false + }, "lean4.automaticallyBuildDependencies": { "type": "boolean", "default": false, @@ -740,60 +745,78 @@ "id": "lean4.welcome.documentation", "title": "Books and Documentation", "description": "Learn using Lean 4 with the resources on the right.", - "media": { "markdown": "./media/guide-documentation.md" } + "media": { + "markdown": "./media/guide-documentation.md" + } }, { "id": "lean4.welcome.installDeps.linux", "title": "Install Required Dependencies", "description": "Install Git and curl using your package manager.", - "media": { "markdown": "./media/guide-installDeps-linux.md" }, + "media": { + "markdown": "./media/guide-installDeps-linux.md" + }, "when": "isLinux" }, { "id": "lean4.welcome.installDeps.mac", "title": "Install Required Dependencies", "description": "Install Homebrew, Git and curl.", - "media": { "markdown": "./media/guide-installDeps-mac.md" }, + "media": { + "markdown": "./media/guide-installDeps-mac.md" + }, "when": "isMac" }, { "id": "lean4.welcome.installDeps.windows", "title": "Install Required Dependencies", "description": "Install Git.", - "media": { "markdown": "./media/guide-installDeps-windows.md" }, + "media": { + "markdown": "./media/guide-installDeps-windows.md" + }, "when": "isWindows" }, { "id": "lean4.welcome.installElan.unix", "title": "Install Lean Version Manager", "description": "Install Lean's version manager Elan.\n[Click to install](command:lean4.setup.installElan)", - "media": { "markdown": "./media/guide-installElan-unix.md" }, + "media": { + "markdown": "./media/guide-installElan-unix.md" + }, "when": "isLinux || isMac" }, { "id": "lean4.welcome.installElan.windows", "title": "Install Lean Version Manager", "description": "Install Lean's version manager Elan.\n[Click to install](command:lean4.setup.installElan)", - "media": { "markdown": "./media/guide-installElan-windows.md" }, + "media": { + "markdown": "./media/guide-installElan-windows.md" + }, "when": "isWindows" }, { "id": "lean4.welcome.setupProject", "title": "Set Up Lean 4 Project", "description": "Set up a Lean 4 project by clicking on one of the options on the right.", - "media": { "markdown": "./media/guide-setupProject.md" } + "media": { + "markdown": "./media/guide-setupProject.md" + } }, { "id": "lean4.welcome.vscode", "title": "Using Lean 4 in VS Code", "description": "Learn how to use Lean 4 together with its VS Code extension.", - "media": { "markdown": "./media/guide-vscode.md" } + "media": { + "markdown": "./media/guide-vscode.md" + } }, { "id": "lean4.welcome.help", "title": "Questions and Troubleshooting", "description": "If you have any questions or are having trouble with any of the previous steps, please visit us on the [Lean Zulip chat](https://leanprover.zulipchat.com/) so that we can help you.", - "media": { "markdown": "./media/guide-help.md" } + "media": { + "markdown": "./media/guide-help.md" + } } ] } diff --git a/vscode-lean4/src/config.ts b/vscode-lean4/src/config.ts index 339e327bf..debd9da0e 100644 --- a/vscode-lean4/src/config.ts +++ b/vscode-lean4/src/config.ts @@ -227,6 +227,10 @@ export function shouldShowInvalidProjectWarnings(): boolean { return workspace.getConfiguration('lean4').get('showInvalidProjectWarnings', true) } +export function getOccurrenceHighlightStringFallback(): boolean { + return workspace.getConfiguration('lean4.editor').get('occurrenceHighlightWithStringFallback', true) +} + export function getLeanExecutableName(): string { if (process.platform === 'win32') { return 'lean.exe' diff --git a/vscode-lean4/src/leanclient.ts b/vscode-lean4/src/leanclient.ts index 90915c566..77e4b9330 100644 --- a/vscode-lean4/src/leanclient.ts +++ b/vscode-lean4/src/leanclient.ts @@ -17,7 +17,7 @@ import { } from 'vscode-languageclient/node' import * as ls from 'vscode-languageserver-protocol' -import { toolchainPath, lakePath, addServerEnvPaths, serverArgs, serverLoggingEnabled, serverLoggingPath, shouldAutofocusOutput, getElaborationDelay, lakeEnabled, automaticallyBuildDependencies } from './config' +import { toolchainPath, lakePath, addServerEnvPaths, serverArgs, serverLoggingEnabled, serverLoggingPath, shouldAutofocusOutput, getElaborationDelay, lakeEnabled, automaticallyBuildDependencies, getOccurrenceHighlightStringFallback } from './config' import { assert } from './utils/assert' import { LeanFileProgressParams, LeanFileProgressProcessingInfo, ServerStoppedReason } from '@leanprover/infoview-api'; import { ExecutionExitCode, ExecutionResult, batchExecute } from './utils/batch' @@ -634,29 +634,30 @@ export class LeanClient implements Disposable { 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) 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, - }) + if (getOccurrenceHighlightStringFallback()) { + // 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) 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; } - - return highlights; } }, }