search

banacorn / agda-mode-vscode

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

Most of the times input field for any command does not work #144

Open uhbif19 opened 1 year ago

uhbif19 commented 1 year ago

Input field is shown, but I cannot type anything into it.

Example: https://www.loom.com/share/bc5cde1440e64882a50238d75aa04a8a

pingbird commented 1 year ago

Downgrading VSCode fixed this for me, the text field just doesn't accept input sometimes

L-TChen commented 1 year ago

I am not able to reproduce using the latest VS code and the extension. Can you try again?

iburzynski commented 1 year ago

I'm having the same issue with VS Codium 1.80.2. When it occurs I need to completely quit Codium and restart to fix it.

pingbird commented 1 year ago

This is happening to me quite frequently still on VSCode 1.80 and agda-mode v0.4.0, not sure what I am doing other than loading agda files and switching panes