checking visible lines and above

Stream: general

[Kevin Buzzard]

Whilst the VS Code option "checking visible lines and above" is probably a useful mode to be in if you're working on a large file, for my users it causes more problems than it solves. I know how to change it to "checking visible files", but every time I open a new folder it changes back. Is there a way to globally change the default once and for all?

[Gabriel Ebner]

There is a setting to change the default. Open user settings and search for lean to see the configuration options.

[Gabriel Ebner]

Maybe we should change the default as well given the troubles it causes.

[Elliott Macneil]

I'm looking at the user settings to change the default.

// Set the default region of interest mode (nothing, visible, lines, linesAndAbove, open, or project) for the Lean extension.
  "lean.roiModeDefault": "linesAndAbove",

It doesn't seem to say what the "checking visible files" option would be - could anyone tell me what that would be?

[Mario Carneiro]

visible is the visible files option