Skip to content

Issues: banacorn/agda-mode-vscode

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

50 Open 90 Closed
50 Open 90 Closed
Author
Filter by author
Loading
Label
Filter by label
Loading
Use alt + click/return to exclude labels
or ⇧ + click/return for logical OR
Projects
Filter by project
Loading
Milestones
Filter by milestone
Loading
Assignee
Filter by who’s assigned
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Issues list

When reopening a folder, the panel created by Agda-mode is restored as an empty window bug Something isn't working
#197 opened Nov 8, 2024 by vic0103520
Support interactive highlighting
#194 opened Oct 3, 2024 by ncfavier
Fails to connect to Agda Language Server on MacOS
#192 opened Sep 5, 2024 by edusporto
Not able to make literate agda file work
#189 opened Aug 24, 2024 by spec-b
Defects in color theme and Unicode characters when deleting text
#188 opened Aug 3, 2024 by GregorPercic
Not (quite) working over web
#187 opened Jun 1, 2024 by yobson
can't type into the normalize expression's text input bug Something isn't working
#186 opened May 14, 2024 by Maylibooyah69
2
Fails to connect to a Agda Language Server running on NixOS on WSL
#183 opened Feb 26, 2024 by VladimirMarko
3
Backslash characters \ are interpreted as escape characters when printed to the agda view bug Something isn't working
#182 opened Feb 24, 2024 by fredrik-bakke
Use multi-chord shortcuts to match Emacs enhancement New feature or request
#181 opened Jan 29, 2024 by nkaretnikov
1
Hightlighting breaks on pretty much any edit bug Something isn't working
#180 opened Jan 11, 2024 by noughtmare
White text on grey background when using light theme bug Something isn't working
#179 opened Jan 8, 2024 by noughtmare
2
\n has started appearing in messages bug Something isn't working
#178 opened Jan 4, 2024 by ncfavier
Download Agda binary if not exists in the path enhancement New feature or request
#170 opened Nov 21, 2023 by L-TChen
3
Holes spanning multiple lines are not handled bug Something isn't working
#159 opened Aug 24, 2023 by fredrik-bakke
3
C-c C-s and C-c C-a inserts \n instead of newlines bug Something isn't working
#158 opened Aug 24, 2023 by fredrik-bakke
3
Nested holes are not highlighted properly bug Something isn't working
#157 opened Aug 24, 2023 by fredrik-bakke
Built-in sorts are highlighted as strings bug Something isn't working
#156 opened Aug 24, 2023 by fredrik-bakke
1
agda is running in read-only (sandboxed?) filesystem bug Something isn't working
#152 opened Aug 17, 2023 by cspollard
3
Most of the times input field for any command does not work bug Something isn't working
#144 opened Jul 7, 2023 by uhbif19
4
Optimistic syntax highlighting enhancement New feature or request
#143 opened Jul 6, 2023 by uhbif19
Unicode Highlight Ambiguous Characters enhancement New feature or request
#142 opened Jun 18, 2023 by fweth
No syntax highlighting? unreproducible please provide more info
#139 opened Mar 28, 2023 by bzm3r
1
From Agda 2.6.4: Simpler way to get Agda version using --numeric-version option enhancement New feature or request
#138 opened Mar 27, 2023 by andreasabel
Building the package locally to use agda-mode input globally question Further information is requested
#137 opened Mar 23, 2023 by inexxt
1
ProTip! Follow long discussions with comments:>50.