VSCode floating infoview

Stream: lean4

[Mario Carneiro]

VSCode finally implemented a long requested feature in the Mar 2024 (1.88) release: floating windows, including for custom editors (i.e. the infoview). Unfortunately, it says:

Note: due to a technical limitation, moving a webview-based editor between windows requires the contents of that editor to reload. It is then up to the editor to restore the state you had previously accumulated. In some cases your state might be reset, as if you had opened the editor for the first time.

and indeed it appears that moving the infoview causes it to permanently get stuck in the initial "Waiting for Lean server to start..." state. So it seems some work is needed on the extension side to make sure that the state is properly reloaded, cc: @Marc Huisinga

[Patrick Massot]

Does it mean we could have the infoview in a separate window? That would be awesome!

[Riccardo Brasca]

Besides putting it in another screen (something I would love to be able to do!), do you have in mind other uses?

[Patrick Massot]

Putting it on another screen is exactly what I have in mind.

[Thomas Murrills]

It also sounds useful when writing non-tactic code (e.g. meta code) on a single screen, where you only occasionally want to flick over to the infoview to see trace messages or something! :)

[Andrés Goens]

FWIW, putting it in a different window works out of the box in emacs (I know it doesn't help if you want to use VScode, but it might help if you care about a two-screen setup more than wether it's vscode or emacs)

[Joël Riou]

Riccardo Brasca said:

Besides putting it in another screen (something I would love to be able to do!), do you have in mind other uses?

I have used a double-screen setup in VScode for several years... (with Linux + fvwm window manager)

double-screen.png

[Patrick Massot]

How do you make sure the info view stays in the right position?

[Enrico Borba]

Joël Riou said:

Riccardo Brasca said:

Besides putting it in another screen (something I would love to be able to do!), do you have in mind other uses?

I have used a double-screen setup in VScode for several years... (with Linux + fvwm window manager)

double-screen.png

This screenshot still looks like it is of a single VS Code window no?

[Joël Riou]

Only one window, but the left half is on a screen, and the right half on another.

[Enrico Borba]

Joël Riou said:

Only one window, but the left half is on a screen, and the right half on another.

Ah gotcha

[Utensil Song]

I can't use the trick above since my setup is like this

image.png

Monitor 2 for long, tall reference stuff where I would place Lean infoview there if this feature is implemented.

[Patrick Massot]

When I tried using a single window on two screen I couldn’t keep the infoview width constant when open or closing it, or when vertically splitting another buffer.