vscode-lean4 RFC: Auto-surround text with `$` in markdown

Stream: general

[Hanson Char]

VS Code currently has a helpful behavior where, if a block of text is selected and the user presses the backtick (``), the selected text is wrapped in backticks rather than replaced.

This RFC proposes extending that behavior to the dollar sign ($) for markdown contexts. Specifically, when text is selected and the user presses $, the editor should wrap the selection in $...$, rather than replacing it with a single dollar sign.

If this sounds useful to you, please let me know! I’d like to open GitHub issue for this and would appreciate support or feedback before doing so.

Thanks!

[Hanson Char]

I've just submitted PR-625 on this.

[Eric Wieser]

This will be quite annoying for `(foo $x $y $z)

[Hanson Char]

The ability to highlight a block of text and enter a dollar sign (to auto surround the block) doesn't affect entering a dollar sign followed by the name of a variable.

[Damiano Testa]

Could this be opt in? I definitely expect to replace my selections by $, rather than enclosing them in $ when writing Lean and the other way round when writing latex.

[Damiano Testa]

If it could be opt-in, I wish the * also was opt-in.

[Hanson Char]

I suppose these can be made as part of the vscode's user preferences so they can be configured via the usual settings.json?

[Damiano Testa]

I'm skeptical about local changes to settings.json, since I think that it is git-tracked.

[Damiano Testa]

Anyway, I added a comment to the issue, since there is surely a way of getting different behaviour, depending on the file type.

[Joscha Mennicken]

Damiano Testa said:

I'm skeptical about local changes to settings.json, since I think that it is git-tracked.

The global settings.json is somewhere in your home directory and specific to you. It is overridden by the repo-specific .vscode/settings.json, which may be tracked in git.

[Damiano Testa]

Ok, so then my opinion is that this change would fit better in a latex vscode setting than in a lean vscode setting.

[Hanson Char]

The VS Code API (specifically with the use of language-configuration.json) currently does not seem to provide a direct way to programmatically modify or reload an already registered language configuration's surroundingPairs array at runtime. May need alternative mechanism to do language config to support dynamic modification.

[Hanson Char]

Opened an RFC.