RFC: Streamlined Entry of LaTeX Math Blocks in Markdown

[hansonchar]

Proposal

This proposal suggests improving the Lean authoring experience by supporting a convenient way to wrap selected Markdown content as a $LaTeX$ math block—e.g., by allowing users to select a block and press $ to wrap it automatically. This is an editor-level improvement aimed at reducing friction when authoring math-rich documentation in Lean.

• User Experience: Entering $LaTeX$ math in Markdown currently requires manually typing $$ before and after each math block, which can be repetitive and error-prone. A simple keyboard interaction to wrap selected content in math delimiters would improve speed and reduce mechanical burden, especially when editing complex mathematical documentation.

• Beneficiaries: Users writing Lean documentation that involves $LateX$ math expressions.

• Maintainability: Will this change streamline code maintenance or simplify its structure? N/A

Community Feedback

Ideas should be discussed on the Lean Zulip prior to submitting a proposal. Summarize all prior discussions and link them here.

Relevant Zulip discussion. Relevant pull request 625.

During the discussion, it was noted that while it would be ideal to allow this behavior to be user-configurable, the current capabilities of VS Code’s language-configuration.json do not expose an API for dynamic reconfiguration. Alternative mechanisms (such as a custom editor command or extension-level configuration) may be necessary to support this feature.

Impact

This proposal aims to improve the productivity of Lean users when working with Markdown and $LaTeX$ math. If you believe this feature would be valuable, please add a 👍 to the issue or share it with others who might benefit.

[mhuisi]

I don't think that there is a nice way to support this feature in a way that is user-configurable, unfortunately.

language-configuration.json is the only API that VS Code provides for this functionality and every implementation that attempts to replicate this behavior by writing text to the editor will be inherently buggy because VS Code lacks atomic read -> write operations for editor contents (our unicode input mechanism is already suffering from a bunch of these and it is a miracle that it works as well as it does).

From reading the VS Code source code, VS Code doesn't have a very smart logic for merging multiple language configurations for the same language either, so you unfortunately can't even write a separate extension that contributes a second language configuration for the lean4 language that includes these additions.

If Lean were to become more deeply integrated with LaTeX, I think it might make sense to provide a separate language ID that includes these adjustments (and additional LaTeX-specific ones) or to even include it in the default lean4 one, but as-is, I'm not sure if there is sufficient motivation to do so.