feat: customizable occurrence highlighting (leanprover#377)

Makes it possible to disable substring-based occurrence highlighting
and use only Lean's compiler responses.

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 <kbd>Ctrl</kbd>+<kbd>Shift</kbd>+<kbd>P</kbd> `Lean 4: Infoview: Display Goal` command.

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,

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'

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;