vscode-lean
vscode-lean copied to clipboard
Change folding style
Currently Lean code is folded like C code, where everything is folded until the next token with less indentation (usually the closing curly brace), including empty lines. That will fold away any separating line breaks between two definitions, making it harder to read. I think the folding style of e. g. Python is better suited for Lean, since we don't have closing curly braces for every indentation level.
VSC has an option for the language-configuration.json file to change that, by adding the option "folding": { "offSide": true }, as mentioned in https://github.com/Microsoft/vscode/issues/3353#issuecomment-330797736.