vscode errors before line is complete

Stream: general

[Rei]

20210417_15h18m10s_grim.png Is there a way to configure the vscode infoview to not reevaluate until the line is complete? I'm having difficulty as the errors while I type remove the tactic state from view

[Rei]

either that or only reevaluate on a command? I took a look at the settings at https://github.com/leanprover/vscode-lean/blob/master/package.json but couldn't find anything similar

[Kevin Buzzard]

Try experimenting with the pause button and the pin (top right).

[Rei]

Yes, the pause button helps, but is there a keyboard shortcut for it?

[Bryan Gin-ge Chen]

You can set one up in the VS Code settings. See https://github.com/leanprover/vscode-lean#info-view-commands for the command names.

[Rei]

Got it, thanks!