vscode-lean icon indicating copy to clipboard operation
vscode-lean copied to clipboard

Change folding style

Open Tasiro opened this issue 5 years ago • 0 comments

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.

Tasiro avatar Nov 09 '20 14:11 Tasiro