You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Add 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 (#762):
'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.
Implement client-side support for planned incremental diagnostic support in the language server (#752)
Fix a bug where the extension would not correctly apply code action snippet edits (#777, author: @Vtec234)
Replace the Lean file icon with the forall icon (#767)
Remove three abbreviations that produce unicode symbols that Mathlib lints against (#764)
Remove HTML highlighting from the Markdown syntax highlighting in Lean doc comments (#770)
Fix a bug where the abbreviation for ⁽ would not trigger ⁽ correctly (#775)
Fix a bug where the Markdown grammar of Lean incorrectly highlighted code after a doc comment (#773)