search

banacorn / agda-mode-vscode

agda-mode on VS Code
https://marketplace.visualstudio.com/items?itemName=banacorn.agda-mode
MIT License
170 stars 40 forks source link

Pressing Enter in Compute normal form input field opens the current file in another tab everytime #202

Closed Dante3085 closed 2 days ago

Dante3085 commented 1 week ago

How to reproduce

  1. Press ctrl-c ctrl-n to open the input field for normalizing an expression.
  2. Put the cursor into the input field if it is not already there and press enter or escape.
  3. You should see another tab open right beside the Agda tab with the input field. This tab will be the current file.

Possible connection with VsCode version

I encountered this problem on my laptop which has the new VsCode version 1.95.3. My other pc didn't have the issue yesterday, but now I checked again and it updated VsCode automatically to that version. Now the issue is there too.

How it looks

Before pressing enter or escape.

image

After pressing enter or escape.

image
banacorn commented 1 week ago

Thank you for the detailed bug report!

Used to be able to just return to the original editor, but now they will open a new editor in the another ViewColumn :(

banacorn commented 1 week ago

I'm considering using the bottom panel though, instead of faking one with an editor

Dante3085 commented 6 days ago

Thank you very much for replying. I really appreciate it!

I just tested VSCode 1.95.3 + agda-mode 0.4.7 and the issue is gone. So, I am not sure whether the issue is the new VSCode version or the latest agda-mode version 0.5.0.

For everyone who wants to quickly fix it before there is a proper fix: As Mark's answer on this Stack Overflow Question explains, you can right-click on an extension in VSCode's extension tab and install a specific version of it.

banacorn commented 5 days ago

Ah! Thanks for the regression testing! Looks like it was my problem after all!

banacorn commented 2 days ago

After hours of tracing and bisecting, it's been fixed at last!