Skip to content

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

Merged
mhuisi merged 1 commit intoleanprover:masterfrom
mhuisi:push-upmprtpksvuu
Apr 15, 2026
Merged

feat: picker-based input method for abbreviations in non-editor contexts#762
mhuisi merged 1 commit intoleanprover:masterfrom
mhuisi:push-upmprtpksvuu

Conversation

@mhuisi
Copy link
Copy Markdown
Collaborator

@mhuisi mhuisi commented Apr 13, 2026

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>
@mhuisi mhuisi merged commit 3861510 into leanprover:master Apr 15, 2026
5 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant