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

46 Open 87 Closed
46 Open 87 Closed
Author
Filter by author
Label
Filter by label
Use alt + click/return to exclude labels
or ⇧ + click/return for logical OR
Projects
Filter by project
Milestones
Filter by milestone
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

can't type into the normalize expression's text input
#186 opened May 14, 2024 by Maylibooyah69
Deactivation of *latex-input*?
#184 opened Mar 25, 2024 by MevenBertrand
Fails to connect to a Agda Language Server running on NixOS on WSL
#183 opened Feb 26, 2024 by VladimirMarko
1
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
editor.action.showDefinitionPreviewHover (Hover or Ctrl+K type information) much slower than it should be. bug Something isn't working
#135 opened Mar 2, 2023 by MathiasSven
Load turns editor split: left/right split into top/bottom split bug Something isn't working
#129 opened Nov 21, 2022 by ChefYeum
2
Customize highlighting levels enhancement New feature or request
#119 opened Sep 4, 2022 by plt-amy
Allow numeric input to complete ambiguous keyboard shortcuts enhancement New feature or request
#117 opened Aug 18, 2022 by thorimur
agda-mode supresses implicit markdown support from vscode question Further information is requested
#108 opened Jun 10, 2022 by andreiburdusa
2
ProTip! What’s not been updated in a month: updated:<2024-04-27.