VSCode Disable Output auto-focus

Stream: lean4

[Mac]

Is there a way to prevent the Lean 4 VSCode extension from auto-focusing the Output pane whenever a new message is printed? I am frequently being tripped up by this behavior as it rips me away from my Integrated Terminal session to show me new log messages (e.g., RPC sessions closures), which can be frustrating.

[Lars König]

There are a lot of GitHub issues about this since there's no option to disable this, but the VSCode team seems to redirect people to the extension developers. Apparently one should set LanguageClientOptions.revealOutputChannelOn to Never and/or call OutputChannel.show with preserveFocus: true, but the second one is already done in the Lean VSCode extension (as far as I can tell) and I just tried the first suggestion, but it doesn't seem to change anything.

[Mac]

Lars König said:

call OutputChannel.show with preserveFocus: true, but [this] one is already done in the Lean VSCode extension (as far as I can tell)

Are you sure? The only uses of preserveFocus I found were not related to the OutputChannel and this line which does use OutputChannel.show does not use preserveFocus.

[Lars König]

Isn't preserveFocus the first argument in this call?

[Wojciech Nawrocki]

@Mac the line you point to does pass preserveFocus : true. This used to be really annoying (it would take the focus away as you write), but I tried it just now and it no longer seems to do so. Are you using VSCode 1.69.2? If so, do you have a repro? I tried it with

elab "ABC" : command => do
  IO.sleep 1000
  unreachable!

[Wojciech Nawrocki]

There is one case where this will still interrupt me - when I have another the Terminal tab open in a pane that also contains Output. For that, you can put them side-by-side within the pane so that the Output is always visible. It's not ideal. Basically the reason why Output is shown is so that users know rather than have to guess if something failed. We could show a message box instead, but that might be even more annoying

[Mac]

Wojciech Nawrocki said:

Basically the reason why Output is shown is so that users know rather than have to guess if something failed.

I would very much prefer I configuration option that determine this. I pretty much never want the Output shown unless I am attempt to debug some server problem. Do you think a PR would be welcome to add such an option?

[Wojciech Nawrocki]

@Mac I guess the right solution here might be to do something like gather stderr, and if the server did fail, show the stderr contents in the infoview. Otherwise it's probably not too relevant and power-users can always inspect it. I would certainly welcome such a PR.

[Wojciech Nawrocki]

I would also welcome a PR simply removing the show output call, but it would be more controversial.

[Mac]

PR is up: https://github.com/leanprover/vscode-lean4/pull/229

[Gabriel Ebner]

I was completely misled by the title here (and of the associated PR). If I understand this correctly, this did not just disable auto-focusing (which I completely agree with) but sneakily also disabled the output panel by default?

That's certainly completely unexpected and problematic since it swallows panics, etc.

[Mac]

Gabriel Ebner said:

If I understand this correctly, this did not just disable auto-focusing (which I completely agree with) but sneakily also disabled the output panel by default?

No, it should just have disabled the auto-focusing/auto-showing of the panel, Lean server output should still be recorded to the panel.

[Mac]

And that is what it does in my experience after updating to v0.0.88 (i.e., I still can view the output by opening the panel).

[Mac]

Also, most errors still pop up as messages boxes anyway, so it doesn't even hide that interruption..

[Chris Lovett]

Mac said:

Also, most errors still pop up as messages boxes anyway, so it doesn't even hide that interruption..

I think the idea is that popping up the output window is much more disruptive to the layout of your editor and the output tab steals the space from the Terminal tab and so on, whereas a message box simply pops on top which is much easier to ignore and close.

[Mac]

@Chris Lovett Yeah, I agree. :smile: My point was that even when not auto-showing the Output pane, users still get foreground notifications on errors, so I am not too worried about users missing the Output auto-show.

[Gabriel Ebner]

No, it should just have disabled the auto-focusing/auto-showing of the panel, Lean server output should still be recorded to the panel.

It is recorded, but silently. In particular, there's no indication whatsoever that the following panics:

#eval (panic! "this should be shown" : Nat)

[Gabriel Ebner]

I think the idea is that popping up the output window is much more disruptive to the layout of your editor and the output tab steals the space from the Terminal tab and so on, whereas a message box simply pops on top which is much easier to ignore and close.

This may be a matter of personal preference. I find the message boxes to be much more disruptive since I have to manually close them, while I can just ignore the output. The three message boxes about failing LSP requests drive me nuts every time the server crashes.

[Gabriel Ebner]

I'd like to change the default of the lean4.autofocusOutput option to true; panics should be shown by default. If I understand this correctly, the concrete issue behind the autofocus option was the RPC session errors which are fixed now: vscode-lean4#236. Are there any other issues that I missed?

[Gabriel Ebner]

Related question: does anybody like the message boxes about failing LSP requests? If not, I'm going to disable them. (Failing LSP requests would still be logged to the output panel, and it would not be auto-focused.)

[Gabriel Ebner]

Also, most errors still pop up as messages boxes anyway, so it doesn't even hide that interruption..

I realize that there may have been some confusion here, because there are multiple kinds of errors and they have different behavior (describing the state before vscode-lean4#229):

• LSP errors: shown as message box, written to output, but not focused (this is the vscode-languageserver's doing)
• Server stderr output: written to output and focused, but no message box (now no longer focused after vscode-lean4#224)
• Lean version info: written to output on startup but not focused

[Mac]

Gabriel Ebner said:

I'd like to change the default of the lean4.autofocusOutput option to true; panics should be shown by default.

I very much do not like this. In my view, UI panes should not be automatically toggling themselves unless I specifically ask them to. Furthermore, most panics from the Lean core and imported libraries (the most common sources, I feel) can't be solved by the user anyway, so having the window pop-up to inform them of this is kind of irrelevant. Finally, auto-showing the Output panel under any circumstances is extremely disruptive, as it can steal focus from e.g., the user typing the Integrated Terminal causing major headaches.

Also, while I admire the attempt to solve all the error messages that emerge. Such appears with relative frequency as both LSP server and extension are updated with new features. Having the extremely disruptive Output panel pop-up to inform users of errors they cannot solve themselves and have to wait until some fix to prevent the disruption seems like bad UX.

If the only reason why the Output panel is auto-shown is to display panics, maybe it would be a better idea to capture messages that begin with "PANIC!" and display them as error boxes instead (and leave the Output panel in its current non-auto-show state).

[Mac]

Gabriel Ebner said:

• Server stderr output: written to output and focused, but no message box (now no longer focused after vscode-lean4#224)

I think the new behavior is reasonable, because outside of debugging the server oneself, most users can not do anything with the information from the stderr, so there is little to no point for them to be presented with it by default.

[Gabriel Ebner]

Furthermore, most panics from the Lean core and imported libraries (the most common sources, I feel) can't be solved by the user anyway

They can't be solved, but they should be reported. It's very much relevant to show them.

because outside of debugging the server oneself, most users can not do anything with the information from the stderr, so there is little to no point for them to be presented with it by default.

The stderr information is almost never from the server (the last two weeks are pretty much the exception, sorry for that). The usual information that's printed on stderr are panics, which you need to address as a user.

[Gabriel Ebner]

extremely disruptive, as it can steal focus from e.g., the user typing the Integrated Terminal

I'm kind of in the opposite boat, since I don't use the integrated terminal at all. Message boxes are much more disruptive to me since they pile up and I need to dismiss them manually, while I can just ignore the output panel. The integrated terminal problem lies partially with vscode. Wojciech writes above that:

This used to be really annoying (it would take the focus away as you write), but I tried it just now and it no longer seems to do so. Are you using VSCode 1.69.2? If so, do you have a repro?

You did not respond to that yet. Does the problem still exist in the latest version?

[Mac]

Gabriel Ebner said:

They can't be solved, but they should be reported. It's very much relevant to show them. .. The usual information that's printed on stderr are panics, which you need to address as a user.

This has not much been my experience. Every time I have encounter the serving reporting a panic, it is due to some weird server edge case (i.e., a partial input that broke something probably)that I have no way of diagnosing or even understanding what caused it. As such, I just continue on as normal and things general continue to work. Showing the panics is to me is just distracting.

[Gabriel Ebner]

Please report them. That's why we show them!!

[Mac]

If I am in the middle of some project I am not going to go bother to do that (and disrupting a user's work flow as means to get users to report Lean bugs seems like bad etiquette). The good news, I guess, is that I have had a panic reported in a while so whatever bugs there were likely got fixed.

[Gabriel Ebner]

Looking at the discussion above, there exist differing preferences for message boxes vs. output panel. We should keep the autofocusOutput option, but also show message boxes on stderr output when it is disabled.

The only question is about the default value. I'm gonna wait a bit and see if anybody else has strong preferences on output panel vs. message boxes.

[Mac]

Gabriel Ebner said:

This used to be really annoying (it would take the focus away as you write), but I tried it just now and it no longer seems to do so. Are you using VSCode 1.69.2? If so, do you have a repro?

You did not respond to that yet. Does the problem still exist in the latest version?

I am using VSCode 1.69.2 and yes I still encountered this (until, of course, v0.0.88 and ceasing of the auto-showing of the Output panel). I do not know what a repro here would look like. If I type in the Terminal and error message is logged to the Output panel, it switches to it and breaks up my input, which is extremely annoying. Because I then have to click on the Terminal (because I don't use keyboard shortcuts for navigation) to go back to typing (which can be quickly disrupted if, like the server has been doing these pasts weeks, more errors come).

[Mario Carneiro]

Mac said:

I very much do not like this. In my view, UI panes should not be automatically toggling themselves unless I specifically ask them to.

(Looks at the goal view...) It bugs me that Ctrl-shift-enter isn't a toggle; when I open a lean file the goal view leaps out of its own volition and I have to use the mouse to get rid of it.

[Mario Carneiro]

I prefer message boxes to the output panel. Especially if something is triggering lots of error messages, the auto-focus can literally prevent me from getting to the terminal to stop the fire

[Mario Carneiro]

I think it is more standard for vscode extensions to show error messages via popup anyway

[Mario Carneiro]

Another possibility, not always applicable, is to use diagnostics though. I think this has a much better user experience and seems appropriate for things like explicit panic! calls

[Gabriel Ebner]

• The autofocusOutput setting default remains false. A surprising number of people use the integrated terminal and it doesn't work well with autofocus, so that's the safer out-of-the-box option.
• However stderr messages produce an error message box now, with a button to open the output panel.
• To balance it out, we don't show error messages for LSP request errors (they still go to the output panel though).
• I've also changed ctrl-shift-enter to be a toggle as requested by Mario.