feat: picker-based input method for abbreviations in non-editor contexts

vscode-lean4/manual/manual.md

@@ -246,6 +246,16 @@ The Unicode input mechanism has several configuration options:
 | :--: | 
 | *Hover for Unicode symbol displaying all abbreviation identifiers* |
 
+To use Unicode symbols outside of text editors - for example in the search bar, find widget or settings - a symbol picker is available. The ['Input: Find Unicode Symbol...'](command:lean4.input.findSymbol) command can be used from the [command menu](#command-menu) or the [command palette](#command-palette). After selecting a symbol, a second dialog allows choosing between copying the symbol to the clipboard and inserting it into the active text editor.
+
+There are also two direct commands that skip the second dialog:
+- ['Input: Insert Unicode Symbol...'](command:lean4.input.insertSymbol) inserts the chosen symbol directly into the active text editor. It is bound to `Ctrl+Alt+\` (`Cmd+Alt+\`) when a text editor is focused.
+- ['Input: Copy Unicode Symbol...'](command:lean4.input.copySymbol) copies the chosen symbol directly to the clipboard. It is bound to `Ctrl+Alt+\` (`Cmd+Alt+\`) when no text editor is focused.
+
+Both direct commands display a button on each item for the other action, so that e.g. a symbol can be copied to the clipboard while using the insert command without having to reopen the dialog.
+
+The search field in the symbol picker supports the same abbreviation identifiers as the regular abbreviation mechanism: typing an abbreviation like `alpha` will find the symbol `α`. The leader character (`\`) can optionally be included. Searching is also possible in reverse by typing or pasting a Unicode symbol to find the abbreviation identifiers that produce it.
+
 ### InfoView
 
 The InfoView is the main interactive component of Lean. It can be used to inspect proof goals, expected types and [diagnostics](#errors-warnings-and-information), as well as render arbitrary user interfaces called ['widgets'](#widgets) for Lean code.

vscode-lean4/package.json

@@ -345,6 +345,24 @@
                 "title": "Convert Current Abbreviation",
                 "description": "Converts the current abbreviation (e.g. \\lam)."
             },
+            {
+                "command": "lean4.input.findSymbol",
+                "category": "Lean 4: Input",
+                "title": "Find Unicode Symbol…",
+                "description": "Opens a dialog to search Unicode abbreviations and lets the user choose to copy or insert the chosen symbol."
+            },
+            {
+                "command": "lean4.input.insertSymbol",
+                "category": "Lean 4: Input",
+                "title": "Insert Unicode Symbol…",
+                "description": "Opens a dialog to search Unicode abbreviations and inserts the chosen symbol into the active editor."
+            },
+            {
+                "command": "lean4.input.copySymbol",
+                "category": "Lean 4: Input",
+                "title": "Copy Unicode Symbol…",
+                "description": "Opens a dialog to search Unicode abbreviations and copies the chosen symbol to the clipboard."
+            },
             {
                 "command": "lean4.displayGoal",
                 "category": "Lean 4: InfoView",
@@ -854,6 +872,18 @@
                 "mac": "tab",
                 "when": "editorTextFocus && lean4.input.isActive"
             },
+            {
+                "command": "lean4.input.insertSymbol",
+                "key": "ctrl+alt+\\",
+                "mac": "cmd+alt+\\",
+                "when": "editorTextFocus"
+            },
+            {
+                "command": "lean4.input.copySymbol",
+                "key": "ctrl+alt+\\",
+                "mac": "cmd+alt+\\",
+                "when": "!editorTextFocus"
+            },
             {
                 "command": "lean4.restartFile",
                 "key": "ctrl+shift+x",
@@ -967,6 +997,16 @@
                     "command": "lean4.input.convert",
                     "when": "lean4.isLeanFeatureSetActive && lean4.input.isActive"
                 },
+                {
+                    "command": "lean4.input.findSymbol"
+                },
+                {
+                    "command": "lean4.input.insertSymbol",
+                    "when": "lean4.input.isTextEditorActive"
+                },
+                {
+                    "command": "lean4.input.copySymbol"
+                },
                 {
                     "command": "lean4.displayGoal",
                     "when": "lean4.isLeanFeatureSetActive"
@@ -1270,10 +1310,15 @@
                     "group": "3_infoview@1"
                 },
                 {
-                    "command": "lean4.loogle.search",
+                    "command": "lean4.input.findSymbol",
                     "when": "config.lean4.alwaysShowTitleBarMenu || lean4.isLeanFeatureSetActive",
                     "group": "4_search@1"
                 },
+                {
+                    "command": "lean4.loogle.search",
+                    "when": "config.lean4.alwaysShowTitleBarMenu || lean4.isLeanFeatureSetActive",
+                    "group": "4_search@2"
+                },
                 {
                     "command": "lean4.troubleshooting.showTroubleshootingGuide",
                     "when": "config.lean4.alwaysShowTitleBarMenu || lean4.isLeanFeatureSetActive",

vscode-lean4/src/abbreviation/AbbreviationFeature.ts

@@ -2,6 +2,7 @@ import { AbbreviationProvider } from '@leanprover/unicode-input'
 import { Disposable, OutputChannel, languages } from 'vscode'
 import { AbbreviationHoverProvider } from './AbbreviationHoverProvider'
 import { AbbreviationRewriterFeature } from './AbbreviationRewriterFeature'
+import { SymbolPickerFeature } from './SymbolPickerFeature'
 import { VSCodeAbbreviationConfig } from './VSCodeAbbreviationConfig'
 
 export class AbbreviationFeature {
@@ -19,6 +20,7 @@ export class AbbreviationFeature {
                 new AbbreviationHoverProvider(config, this.abbreviations),
             ),
             new AbbreviationRewriterFeature(config, this.abbreviations, outputChannel),
+            new SymbolPickerFeature(config, this.abbreviations),
         )
     }