agda-mode-vscode

agda-mode-vscode copied to clipboard

Setting agda path to `docker run...` gets ignored, reverts to local CLI

2

I have agda installed locally and also have created a docker image which I am testing. I set the agda path to `docker run -i --rm agda-2.6.2 agda` similar to...

glangmead

Goto definition won't work on Windows

11

As title.

ice1000

Debug buffer prints more then necessary

1

The debug buffer prints 1. modules being checked and 2. a number apart from the actual information printed to the debug buffer. Can you remove these two parts?

L-TChen

load (c-c c-l) is stuck with "Loading .."

5

I had vs code with agda-mode working - installed following instructions on a system build with debian and using cabal. Then I deleted the `.cabal/store` folder (it had accumulated too...

andrewufrank

Links don't work in the error messages.

5

 In the picture, If I hover the mouse over the reference line (blue link), nothing happens. Of course, I go myself the way to that line, but the cursor...

jonaprieto

Dead keys

4

I have an issue that some of my keys/keybindings no longer work during/after using `agda-mode`: - `\` (in search bar) - `(` - `)` - `C-x` - `C-c` This doesn't...

barrettj12

Scroll down in the Agda Debug Buffer panel

1

Hello, I've been enjoying this extension quite a bit, thanks for the work! Recently I started using the debug buffer panel, to view the contents of the debug buffer. I...

pvdstel

Unicode input in find/replace

2

At the moment, Unicode input doesn't work in find/replace. While this would be nice to have (if possible), it's not essential. The real problem is that `\` still starts Unicode...

barrettj12

Syntax highlighting doesn't update correctly when filling a hole until the file is reloaded with C-c C-l

1

 After filling a hole with something, and hitting `C-c C-SPC` (give) or `C-c C-r` (refine) the syntax highlighting is extremely wrong, with individual characters or groups of characters being...

natronium

Unicode input mode doesn't reactivate when ended with backslash (ie to enter a second adjacent character)

1

Hitting `\` seems to complete my unicode input, but it doesn't start a new one. If I want to type `≡⟨⟩` currently, I need to press: `\==ESC\` which is a...

natronium