VSCode Infoview in a new window

Stream: new members

[Pedro Sánchez Terraf]

Hi everyone, I've installed Lean 3 for my Debian (testing) system, and I'm new to VSCode (I'm a regular Emacs user, but I tried to do everything recommended in the installation guide).

How do you separate the Infoview tab from the window where the corresponding .lean file is being edited?

I'm able to drag & drop the tab containing the file to another window, but that opens a new Infoview in that window. I'm sorry for such a basic question, but after googling, SOing and searching here I could not find an answer.

[Kevin Buzzard]

Try closing the infoview and then reopening it by clicking on the funny funny.png symbol.

[Kevin Buzzard]

infoview.gif Is this what you're asking to do or did I misunderstand?

[Pedro Sánchez Terraf]

Thank you very much, Kevin. Though, it seems that clicking on that opens the Infoview again in the same window.

What I'd rather is a separate window with the Infoview, in order to move it to another screen (while I edit the Lean file on my laptop screen).

[Jireh Loreaux]

I don't think it's possible to open the infoview in a new window (I think different VS Code windows are separate processes, but I might be wrong), but maybe someone will enlighten me.

[Riccardo Brasca]

You can make the VS Code window so big that it is in both screens, and the organize the tab to have the infoview in one screen and the rest in the other

[Pedro Sánchez Terraf]

Riccardo Brasca said:

You can make the VS Code window so big that it is in both screens

Yeah I thought about this :sweat_smile: but then, there should be a cleverer way, shouldn't it?

Edit: Oh, also, the height of the two screens do not match :sad:

[Riccardo Brasca]

Yes it's just a workaround...

[Patrick Massot]

I tried that workaround in the very beginning and it didn't work. I was painful to keep the boundary at the correct position.

[Chris Lovett]

The way VS code works is a single window is tied to a single language server. When you use File/New Window you are creating an entirely new instance of VS code which will create it's own entirely new language server (for example these could be browsing different folders with different versions of lean, or better yet, one vs code is browsing a local folder while the other is connected via SSH to a remote folder on another machine!). So, the InfoView then is tied to one VS code window only and cannot be drag/dropped out to a different monitor. This is kind of a limitation of how VS code works (unfortunately). So, folks like me end up with a huge curved monitor so that a full screen VS code feels like 2 monitors :-)