feat: picker-based input method for abbreviations in non-editor contexts (#762)

This PR adds three new abbreviation-related commands that have the goal
of making it easier to insert Unicode symbols into non-editor dialogs
and to make abbreviations more discoverable:
- 'Find Unicode Symbol...': Displays a picker dialog that allows
searching for Unicode symbols either by abbreviation or by symbol.
Selecting an entry then provides an option to either copy the symbol or
to insert it into the currently active text editor. Displayed in the
forall menu.
- 'Copy Unicode Symbol...': Like 'Find Unicode Symbol', but selecting a
symbol from the dialog immediately copies it instead of opening another
dialog to choose whether the symbol should be inserted or copied. Bound
to Ctrl+Alt+\ when no text editor is focused.
- 'Insert Unicode Symbol...': Like 'Find Unicode Symbol', but selecting
a symbol from the dialog immediately inserts it instead of opening
another dialog to choose whether the symbol should be inserted or
copied. Bound to Ctrl+Alt+\ when a text editor is focused.

Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>

Author: mhuisi

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),
         )
     }