issues
search
banacorn
/
agda-mode-vscode
agda-mode on VS Code
https://marketplace.visualstudio.com/items?itemName=banacorn.agda-mode
MIT License
167
stars
38
forks
source link
issues
Newest
Newest
Most commented
Recently updated
Oldest
Least commented
Least recently updated
No syntax highlighting?
#139
bzm3r
opened
1 year ago
1
From Agda 2.6.4: Simpler way to get Agda version using `--numeric-version` option
#138
andreasabel
opened
1 year ago
0
Building the package locally to use agda-mode input globally
#137
inexxt
opened
1 year ago
1
Bump webpack from 5.74.0 to 5.76.0
#136
dependabot[bot]
closed
1 year ago
0
`editor.action.showDefinitionPreviewHover` (Hover or `Ctrl+K` type information) much slower than it should be.
#135
MathiasSven
opened
1 year ago
0
Bump json5 from 2.2.1 to 2.2.3
#133
dependabot[bot]
closed
1 year ago
0
Agda Mode Keyboard Shortcuts does not Work Except Loading a File
#132
Naruyoko
closed
1 year ago
11
Add "!editorHasSelection" condition to agda-mode.lookup-symbol
#131
jespercockx
closed
1 year ago
1
Tighten up the layout in the bottom panel.
#130
dunhamsteve
closed
1 year ago
1
Load turns editor split: left/right split into top/bottom split
#129
ChefYeum
opened
1 year ago
2
Bump loader-utils from 2.0.2 to 2.0.4
#128
dependabot[bot]
closed
1 year ago
0
Bump loader-utils from 2.0.2 to 2.0.3
#127
dependabot[bot]
closed
1 year ago
1
[ fix ] Update language-server-mule to 0.2.4 (Fixes LSP)
#126
jul1u5
closed
8 months ago
6
Modal bindings are not shown in the goal context
#125
plt-amy
closed
8 months ago
1
Agda files are not Markdown files
#124
plt-amy
closed
1 year ago
1
Added logo
#123
Trebor-Huang
closed
1 year ago
1
Error starting the language server
#122
damienstanton
closed
8 months ago
6
add lagda.md highlight support
#121
choukh
closed
1 year ago
1
Icon for agda files (and for the extension itself)
#120
Trebor-Huang
closed
1 year ago
2
Customize highlighting levels
#119
plt-amy
opened
1 year ago
0
Syntax highlighting for COMPILE and FOREIGN pragmas
#118
KislyjKisel
closed
1 year ago
1
Allow numeric input to complete ambiguous keyboard shortcuts
#117
thorimur
opened
2 years ago
0
Agda Language Server stopped working after 0.3.10 update
#116
mz71
closed
8 months ago
0
[ fix ] "go to definition" on Windows
#115
mz71
closed
2 years ago
1
Fix typos of 'Shortcuts' in documentation
#114
pragma-
closed
2 years ago
2
Bump terser from 5.7.1 to 5.14.2
#113
dependabot[bot]
closed
2 years ago
0
Don't store the agda path in the config
#112
ncfavier
closed
2 years ago
3
Fix the documentation for the case split keymap
#111
stepchowfun
closed
2 years ago
1
"Shortcut" is typoed as "Shortcurs"
#110
pragma-
closed
2 years ago
3
remove "machine-overridable" scope from some settings
#109
kzvi
closed
2 years ago
1
agda-mode supresses implicit markdown support from vscode
#108
andreiburdusa
opened
2 years ago
2
Prevent expressions from being quoted twice
#107
pvdstel
closed
2 years ago
1
Loading can fail silently
#106
joliss
opened
2 years ago
1
Case Split not working
#105
GetContented
closed
2 years ago
4
VSCode does not display results of ctrl-C, ctrl-L or ctrl-C, ctrl-P
#104
jxxcarlson
opened
2 years ago
3
Bump async from 3.2.1 to 3.2.3
#103
dependabot[bot]
closed
2 years ago
0
Bump ansi-regex from 3.0.0 to 3.0.1
#102
dependabot[bot]
closed
2 years ago
0
Use user-specified font family
#101
plt-amy
closed
2 years ago
1
Jump to the middle of goals
#100
ncfavier
closed
2 years ago
5
No backend called 'GHC' (installed backends: GHCNoMain, QuickLaTeX)
#99
brando90
opened
2 years ago
4
can't compile agda in vscode anymore
#98
brando90
closed
2 years ago
1
`command 'agda-mode.load' not found` with working Agda installation
#97
timvandam
closed
2 years ago
2
Bump minimist from 1.2.5 to 1.2.6
#96
dependabot[bot]
closed
2 years ago
0
Wrong colors in light theme
#95
cad0p
opened
2 years ago
2
Error: `AbstractContextKeyService` has been disposed
#94
ruifengx
closed
2 years ago
10
Setting agda path to `docker run...` gets ignored, reverts to local CLI
#93
glangmead
opened
2 years ago
2
Properly handle GetOs
#92
ThePuzzlemaker
closed
2 years ago
1
Error when loading with LSP enabled: `Cannot read property 'dist' of null`
#91
ThePuzzlemaker
closed
2 years ago
0
Debug buffer prints more then necessary
#90
L-TChen
opened
2 years ago
1
Bump shelljs from 0.8.4 to 0.8.5
#89
dependabot[bot]
closed
2 years ago
0
Previous
Next