Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Restarting server resets position of goal window #678

Open
Alizter opened this issue Apr 15, 2024 · 2 comments · Fixed by #755
Open

Restarting server resets position of goal window #678

Alizter opened this issue Apr 15, 2024 · 2 comments · Fixed by #755
Labels
Milestone

Comments

@Alizter
Copy link
Collaborator

Alizter commented Apr 15, 2024

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
Copy link
Owner

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.

@ejgallego ejgallego added this to the 0.2.0 milestone Jun 8, 2024
@ejgallego ejgallego linked a pull request Jun 8, 2024 that will close this issue
@Alizter
Copy link
Collaborator Author

Alizter commented Jun 8, 2024

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.

@ejgallego ejgallego modified the milestones: 0.2.0, 0.2.1 Jun 9, 2024
@ejgallego ejgallego modified the milestones: 0.2.1, 0.2.2 Sep 26, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

Successfully merging a pull request may close this issue.

2 participants