Extension for VS Code that provides support for the older Lean 3 language. Succeeded by vscode-lean4 ('lean4' in the extensions menu) for the Lean 4 language.
Apache License 2.0
116
stars
49
forks
source link
Lines of tildes in comments screw up Lean parsing in this plugin #336
/-
~~~
-/
def x := 1 -- code highlighting no longer works and other stuff breaks, too.
This is a problem because lines of tildes are used as subsection markup in RestructuredText documents, which J. Avigad and others are using to format Lean files as presentable documents.
This is a consequential bug, and given the simplicity of the test cases here, should be pretty easy to track down.
This works fine:
Add one more tilde and important stuff breaks.
This is a problem because lines of tildes are used as subsection markup in RestructuredText documents, which J. Avigad and others are using to format Lean files as presentable documents.
This is a consequential bug, and given the simplicity of the test cases here, should be pretty easy to track down.
Thank you, Kevin Sullivan University of Virginia