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

agda-mode on VS Code

Results 56 agda-mode-vscode issues
Sort by recently updated
recently updated
newest added

As title. It seems that CI on Windows failed before testing since it cannot download vscode. Is there any solution? ![CI](https://github.com/banacorn/agda-mode-vscode/assets/46051434/4f4b95b9-61b6-43b5-8aaf-fa3185eff93b)

I just installed agda-mode in VS Code, but I am not getting any syntax highlighting: ![image](https://user-images.githubusercontent.com/4350451/228210800-8ed7029e-7bd1-4190-b745-4995fd248ecd.png) Why is this?

unreproducible

Improve how Agda buffer appear: - This modification preserves current layout and create a new panel depending on configuration or current layout. For example, - if there's only one editor,...

dependencies

Nested holes are highlighted only from the first opening to the first closing bracket. Example:

bug

Built-in sorts are highlighted as strings, but shouldn't be: I suggest using a scope like `support.type.sort.agda` instead.

bug

Hello, First, let me thank you for writing and maintaining this extension: agda would be very difficult without it. I've noticed that system calls via the Reflection.External interface fail if...

bug

Input field is shown, but I cannot type anything into it. Example: https://www.loom.com/share/bc5cde1440e64882a50238d75aa04a8a

bug

## Steps to reproduce 1. Open an Agda file 2. Split screen left/right: Either via drag & drop or with VSCode command `View: Split Editor Right` 3. Run `Agda: Load`...

bug

Every time (or most of times) when load fails, syntax highlighting stops working. Could not it just not change if load is not successful? That will also make various auto-load...

enhancement

Hi, it seems like the extension doesn't change VSCode's "highlight ambiguous characters" feature. It's not a big deal since you can disable the feature manually for certain languages, but other...

enhancement