Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR adjusts the
language-configuration.json
to automatically insert a closing bracket when typing\<
, automatically triggering the\<>
abbreviation, making it look like we auto-closed⟨
. The only downside of this approach is that then deleting⟨
will not delete the corresponding⟩
(as would be the case with actual auto-closed brackets), but implementing this is a lot more difficult, since sending edits to VS Code is often subject to race conditions (c.f. #389).We unfortunately cannot use this approach for
\f<
and\f<<
as VS Code would always automatically auto-close\f<
due to the common prefix, making it impossible to type\f<<
.Resolves #331.