feat: customizable occurrence highlighting

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,
@@ -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"
+						}
 					}
 				]
 			}

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;