agda-mode-vscode icon indicating copy to clipboard operation
agda-mode-vscode copied to clipboard

Published 20 hours ago • verified publisher icon banacorn

Links don't work in the error messages.

Open jonaprieto opened this issue 4 years ago • 5 comments

image

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 should go after clicking that the link.

jonaprieto avatar Nov 17 '20 18:11 jonaprieto

Yep notices the same problem in agda-mode 0.2.3

bblfish avatar Jan 02 '21 16:01 bblfish

I'm still having this issue. Should the fix already be in the version of the extension on the vscode marketplace?

The bug was closed with a patch on Sep 26, and the extension was last updated on Sep 27. Does that mean the fix doesn't work for me?

jonas-frey avatar Oct 04 '21 16:10 jonas-frey

@jonas-frey, thanks for reporting this. Are you using Windows?

banacorn avatar Oct 05 '21 02:10 banacorn

@banacorn : I'm using ubuntu 21.04 with kde.

jonas-frey avatar Oct 05 '21 15:10 jonas-frey

I'm having the same issue on Ubuntu 21.10 with GNOME. I'd also love an option to automatically follow such links, like how the cursor automatically jumps to the first error in the same file, but across files.

jliptrap avatar Jan 04 '22 23:01 jliptrap