From ceccfe7232234836e32488e074ed8273043b5c77 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Tue, 9 Jan 2024 10:01:37 +0100 Subject: [PATCH] feat: customizable occurrence highlighting (#377) Makes it possible to disable substring-based occurrence highlighting and use only Lean's compiler responses. --- README.md | 2 ++ vscode-lean4/package.json | 5 +++++ vscode-lean4/src/config.ts | 4 ++++ vscode-lean4/src/leanclient.ts | 10 +++++++--- 4 files changed, 18 insertions(+), 3 deletions(-) diff --git a/README.md b/README.md index 36075c8de..1cd5f2df7 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.fallBackToStringOccurrenceHighlighting`: 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 60e6a99be..073a3067f 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.fallBackToStringOccurrenceHighlighting": { + "type": "boolean", + "description": "Fall back to string-based occurrence highlighting when there are no semantic symbol occurrences from the Lean language server to highlight.", + "default": false + }, "lean4.automaticallyBuildDependencies": { "type": "boolean", "default": false, diff --git a/vscode-lean4/src/config.ts b/vscode-lean4/src/config.ts index 339e327bf..b457c3835 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 getFallBackToStringOccurrenceHighlighting(): boolean { + return workspace.getConfiguration('lean4').get('fallBackToStringOccurrenceHighlighting', false) +} + 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 c5f72263c..cb43e548f 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, getFallBackToStringOccurrenceHighlighting } from './config' import { assert } from './utils/assert' import { LeanFileProgressParams, LeanFileProgressProcessingInfo, ServerStoppedReason } from '@leanprover/infoview-api'; import { ExecutionExitCode, ExecutionResult, batchExecute } from './utils/batch' @@ -635,8 +635,12 @@ export class LeanClient implements Disposable { 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 + // vscode doesn't fall back to textual highlights, so we + // need to do that manually if the user asked for it + if (!getFallBackToStringOccurrenceHighlighting()) { + return []; + } + await new Promise((res) => setTimeout(res, 250)); if (ctok.isCancellationRequested) return;