Lean server mode in VS Code

Stream: general

[Moses Schönfinkel]

So a strange thing has just started happening to me - whenever I open a window in VS Code with an instance of lean server, it arbitrarily chooses between a mode that displays all messages at the same time + moving the cursor doesn't do anything, as everything is displayed and between the "interactive" mode, where cursor determines what messages and / or proof state is displayed. Anybody has encountered this - is there a way to force default? Am I going completely insane? (don't answer the latter).

[Chris Hughes]

These two buttons switch between the two modes Screenshot-2019-01-23-at-08.14.24.png

[Moses Schönfinkel]

Thank you, I must have been somehow accidentally pressing their what appears to be an accidentally-unpressable shortcut.