From f8c9459dddd08b7f448370834c84488a239ff538 Mon Sep 17 00:00:00 2001 From: Kenny Lau Date: Mon, 27 Oct 2025 01:06:11 +0000 Subject: [PATCH 1/2] Update manual with PR instructions for abbreviations Added instructions for modifying abbreviation identifiers. --- vscode-lean4/manual/manual.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/vscode-lean4/manual/manual.md b/vscode-lean4/manual/manual.md index 284ad816..dd3e875b 100644 --- a/vscode-lean4/manual/manual.md +++ b/vscode-lean4/manual/manual.md @@ -213,7 +213,7 @@ Lean code uses lots of [Unicode symbols](https://home.unicode.org/) to aid reada To replace an abbreviation early, before it is complete, `Tab` can be pressed to trigger the ['Input: Convert Current Abbreviation'](command:lean4.input.convert) command. This will yield the Unicode symbol with the shortest abbreviation identifier matching the identifier that was typed. Abbreviations are also replaced early when the text cursor is moved away from the abbreviation. -The full list of supported abbreviation identifiers and Unicode symbols can be viewed using the ['Docs: Show Unicode Input Abbreviations'](command:lean4.docs.showAbbreviations) command that can be found in the 'Documentation…' submenu of the command menu. When encountering a Unicode symbol in Lean code, [hovering](#hovers) over the symbol will also provide all available abbreviation identifiers to input the symbol. +The full list of supported abbreviation identifiers and Unicode symbols can be viewed using the ['Docs: Show Unicode Input Abbreviations'](command:lean4.docs.showAbbreviations) command that can be found in the 'Documentation…' submenu of the command menu. When encountering a Unicode symbol in Lean code, [hovering](#hovers) over the symbol will also provide all available abbreviation identifiers to input the symbol. If you wish to add new abbreviations or modify existing abbreviations, please make a PR to modify [vscode-lean4/lean4-unicode-input/src/abbreviations.json](https://github.com/leanprover/vscode-lean4/blob/master/lean4-unicode-input/src/abbreviations.json). For some Unicode brackets, there are special abbreviation identifiers that also insert a matching closing Unicode bracket and ensure that the cursor is in-between the Unicode brackets after replacing the abbreviation. For example, `\<>` yields `⟨⟩`, `\[[]]` yields `⟦⟧`, `\f<<>>` yields `«»` and `\norm` yields `‖‖`. From 3e3c6a8e0f95e7b046e402f62d8b7dbfa4259fc6 Mon Sep 17 00:00:00 2001 From: Kenny Lau Date: Mon, 27 Oct 2025 01:16:04 +0000 Subject: [PATCH 2/2] Clarify abbreviation modification process in manual Updated instructions for modifying abbreviation identifiers and added a discussion step on Zulip. --- vscode-lean4/manual/manual.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/vscode-lean4/manual/manual.md b/vscode-lean4/manual/manual.md index dd3e875b..5197ddf4 100644 --- a/vscode-lean4/manual/manual.md +++ b/vscode-lean4/manual/manual.md @@ -213,7 +213,7 @@ Lean code uses lots of [Unicode symbols](https://home.unicode.org/) to aid reada To replace an abbreviation early, before it is complete, `Tab` can be pressed to trigger the ['Input: Convert Current Abbreviation'](command:lean4.input.convert) command. This will yield the Unicode symbol with the shortest abbreviation identifier matching the identifier that was typed. Abbreviations are also replaced early when the text cursor is moved away from the abbreviation. -The full list of supported abbreviation identifiers and Unicode symbols can be viewed using the ['Docs: Show Unicode Input Abbreviations'](command:lean4.docs.showAbbreviations) command that can be found in the 'Documentation…' submenu of the command menu. When encountering a Unicode symbol in Lean code, [hovering](#hovers) over the symbol will also provide all available abbreviation identifiers to input the symbol. If you wish to add new abbreviations or modify existing abbreviations, please make a PR to modify [vscode-lean4/lean4-unicode-input/src/abbreviations.json](https://github.com/leanprover/vscode-lean4/blob/master/lean4-unicode-input/src/abbreviations.json). +The full list of supported abbreviation identifiers and Unicode symbols can be viewed using the ['Docs: Show Unicode Input Abbreviations'](command:lean4.docs.showAbbreviations) command that can be found in the 'Documentation…' submenu of the command menu. When encountering a Unicode symbol in Lean code, [hovering](#hovers) over the symbol will also provide all available abbreviation identifiers to input the symbol. If you wish to add new abbreviations or modify existing abbreviations, please first discuss it on [Zulip](https://leanprover.zulipchat.com/), and then make a PR to modify [vscode-lean4/lean4-unicode-input/src/abbreviations.json](https://github.com/leanprover/vscode-lean4/blob/master/lean4-unicode-input/src/abbreviations.json). For some Unicode brackets, there are special abbreviation identifiers that also insert a matching closing Unicode bracket and ensure that the cursor is in-between the Unicode brackets after replacing the abbreviation. For example, `\<>` yields `⟨⟩`, `\[[]]` yields `⟦⟧`, `\f<<>>` yields `«»` and `\norm` yields `‖‖`.