search

ejgallego / coq-lsp

Visual Studio Code Extension and Language Server Protocol for Coq
GNU Lesser General Public License v2.1
143 stars 31 forks source link

Restarting server resets position of goal window #678

Open Alizter opened 4 months ago

Alizter commented 4 months ago

I'm not sure if this is a VSCode bug or something we can fix in the coq-lsp.

Problem

When you restart the coq-lsp server, the goals window closes and opens which means that it ends up getting grouped with your tab group rather than being on the side.

Here is before restarting:

image

here is after restarting:

image

Fix

It would be nice if we didn't have to manually fix this every time we restart.

Of course, another way to fix this is not to have to restart so often, but this issue is still somewhat annoying.

Workarounds

One workaround I've been doing is to have an unrelated tab open in the same tab group so that the group doesn't collapse when the goals panel is closed. That way the alignment and width can be preserved. Of course, the goals panel will appear in whatever buffer you are currently selecting which means you still have to move it.

ejgallego commented 3 months ago

I cannot reproduce in vscode 1.90 , is that still a problem for you @Alizter ?

I think this may have been fixed by #755 and related PRs.

Alizter commented 3 months ago

Yes this appears to be fixed, but not by #755 IIUC. On my version there is a race that #755 is supposed to fix I see.

There is a related issue where you have 3 buffers horizontally and you restart, it turns into 2 and then opens a new tab for the goals on the right buffer rather than returning the 3 from before.