Ecosyste.ms: Issues
An open API service for providing issue and pull request metadata for open source projects.
GitHub / banacorn/agda-mode-vscode issues and pull requests
#211 - Nested comments confuse the parser
Issue -
State: open - Opened by ncfavier 3 days ago
#210 - [ fix ] Don't add padding to goal brackets
Pull Request -
State: open - Opened by ncfavier 5 days ago
#209 - agda-mode should work offline
Issue -
State: open - Opened by phadej 5 days ago
#208 - Basic `lagda.typ` support
Pull Request -
State: open - Opened by mzhang28 10 days ago
#207 - Filling a hole with identifier >= 10 sometimes incorrectly keeps `!` and consumes following character
Issue -
State: open - Opened by HarrisonGrodin 24 days ago
- 5 comments
#206 - Update README.md to reflect the changes made in bea7cbe
Pull Request -
State: open - Opened by tsung-ju about 1 month ago
#205 - "Unbound variable x!" when trying to case split on x
Issue -
State: open - Opened by andreasabel 2 months ago
- 1 comment
#204 - Bad state after C-c C-s (solve)
Issue -
State: open - Opened by andreasabel 2 months ago
#203 - Ability to Normalize an expression within the current scope
Issue -
State: open - Opened by laserbat 2 months ago
#202 - Pressing Enter in Compute normal form input field opens the current file in another tab everytime
Issue -
State: closed - Opened by Dante3085 3 months ago
- 5 comments
Labels: bug
#201 - Agda Auto fails for multiline code
Issue -
State: open - Opened by CSchank 3 months ago
- 1 comment
Labels: bug, unreproducible
#200 - Fix year in CHANGELOG.md
Pull Request -
State: closed - Opened by fredrik-bakke 3 months ago
- 1 comment
#199 - Fix '\n' in panel and refinement output
Pull Request -
State: closed - Opened by jiangsy 3 months ago
- 2 comments
#198 - Address several warnings during build
Pull Request -
State: closed - Opened by jiangsy 3 months ago
- 1 comment
#197 - When reopening a folder, the panel created by Agda-mode is restored as an empty window
Issue -
State: closed - Opened by vic0103520 4 months ago
- 2 comments
Labels: bug
#197 - When reopening a folder, the panel created by Agda-mode is restored as an empty window
Issue -
State: open - Opened by vic0103520 4 months ago
Labels: bug
#196 - Improve the logic related to buffer's font size adjustment
Pull Request -
State: closed - Opened by jiangsy 4 months ago
- 1 comment
#196 - Improve the logic related to buffer's font size adjustment
Pull Request -
State: closed - Opened by jiangsy 4 months ago
- 1 comment
#195 - Remove all usage of deprecated api @bs.send.pipe
Pull Request -
State: closed - Opened by jiangsy 4 months ago
- 1 comment
#194 - Support interactive highlighting
Issue -
State: open - Opened by ncfavier 5 months ago
#193 - Agda Auto doesn't work with Agda 2.7.0
Issue -
State: closed - Opened by CMDJojo 5 months ago
- 2 comments
#192 - Fails to connect to Agda Language Server on MacOS
Issue -
State: open - Opened by edusporto 6 months ago
#191 - Add more detailed splitting command description
Pull Request -
State: closed - Opened by ChAoSUnItY 6 months ago
- 1 comment
#190 - Bump webpack from 5.89.0 to 5.94.0
Pull Request -
State: open - Opened by dependabot[bot] 6 months ago
Labels: dependencies
#189 - Not able to make literate agda file work
Issue -
State: open - Opened by spec-b 6 months ago
#188 - Defects in color theme and Unicode characters when deleting text
Issue -
State: open - Opened by GregorPercic 7 months ago
#187 - Not (quite) working over web
Issue -
State: open - Opened by yobson 9 months ago
#186 - can't type into the normalize expression's text input
Issue -
State: open - Opened by Maylibooyah69 9 months ago
- 2 comments
Labels: bug
#185 - On Linux, agda-mode hijack the keybinding
Issue -
State: closed - Opened by dannypsnl 11 months ago
- 1 comment
#184 - Deactivation of *latex-input*?
Issue -
State: closed - Opened by MevenBertrand 11 months ago
- 2 comments
#183 - Fails to connect to a Agda Language Server running on NixOS on WSL
Issue -
State: open - Opened by VladimirMarko 12 months ago
- 3 comments
#182 - Backslash characters `\` are interpreted as escape characters when printed to the agda view
Issue -
State: open - Opened by fredrik-bakke 12 months ago
Labels: bug
#181 - Use multi-chord shortcuts to match Emacs
Issue -
State: closed - Opened by nkaretnikov about 1 year ago
- 2 comments
Labels: enhancement
#180 - Hightlighting breaks on pretty much any edit
Issue -
State: open - Opened by noughtmare about 1 year ago
Labels: bug
#179 - White text on grey background when using light theme
Issue -
State: open - Opened by noughtmare about 1 year ago
- 2 comments
Labels: bug
#178 - `\n` has started appearing in messages
Issue -
State: closed - Opened by ncfavier about 1 year ago
Labels: bug
#177 - [ fix #176 ] Update `asset/keymap.js`
Pull Request -
State: closed - Opened by szumixie about 1 year ago
#176 - Many Unicode input sequences no longer work
Issue -
State: closed - Opened by szumixie about 1 year ago
- 1 comment
Labels: bug
#175 - Refining a goal having `\` (instead of `λ`) results in an Internal Parse Error
Issue -
State: closed - Opened by scmu about 1 year ago
- 1 comment
Labels: bug
#174 - `C-c` `C-l` causes it to keep loading, and typing it again will get an S-expression parsing failure.
Issue -
State: closed - Opened by vbcpascal about 1 year ago
- 1 comment
Labels: bug
#173 - `C-c` `C-r` results in wrong character when applied to character outside of BMP
Issue -
State: closed - Opened by choukh about 1 year ago
- 3 comments
Labels: bug
#172 - "Connection Error: Unable to find Agda Language Server" Error downloading language server?
Issue -
State: closed - Opened by N10KYA about 1 year ago
- 4 comments
Labels: bug
#171 - `asset/keymap.js` is outdated/incomplete compared to Agda's emacs-mode
Issue -
State: closed - Opened by fredrik-bakke about 1 year ago
- 4 comments
Labels: enhancement
#170 - Download Agda binary if not exists in the path
Issue -
State: open - Opened by L-TChen over 1 year ago
- 3 comments
Labels: enhancement
#169 - Custom Agda buffer font size in the extension's setting
Pull Request -
State: closed - Opened by vic0103520 over 1 year ago
- 2 comments
#168 - LSP Stuck on Loading
Issue -
State: closed - Opened by aricursion over 1 year ago
- 3 comments
Labels: bug, duplicate
#167 - Make the font size of Agda buffer the same as editors
Pull Request -
State: closed - Opened by vic0103520 over 1 year ago
- 1 comment
Labels: enhancement
#166 - Re #90: Debug buffer won't print modules checked and verbosity
Pull Request -
State: closed - Opened by vic0103520 over 1 year ago
#165 - Case split does not reload
Issue -
State: closed - Opened by ncfavier over 1 year ago
- 2 comments
Labels: bug, unreproducible
#164 - Case splitting holes after a new line are mishandled
Issue -
State: closed - Opened by fredrik-bakke over 1 year ago
- 3 comments
#163 - Define auto indentation rules
Pull Request -
State: closed - Opened by fredrik-bakke over 1 year ago
- 5 comments
#162 - Autoclosing parentheses and curly braces interferes with agda-input
Issue -
State: closed - Opened by fredrik-bakke over 1 year ago
#161 - Compact UI
Pull Request -
State: closed - Opened by fredrik-bakke over 1 year ago
- 3 comments
#160 - Agda-mode pane is too space inefficient
Issue -
State: closed - Opened by fredrik-bakke over 1 year ago
#159 - Holes spanning multiple lines are not handled
Issue -
State: open - Opened by fredrik-bakke over 1 year ago
- 3 comments
Labels: bug
#158 - `C-c` `C-s` and `C-c` `C-a` inserts `\n` instead of newlines
Issue -
State: closed - Opened by fredrik-bakke over 1 year ago
- 3 comments
Labels: bug
#157 - Nested holes are not highlighted properly
Issue -
State: open - Opened by fredrik-bakke over 1 year ago
Labels: bug
#156 - Built-in sorts are highlighted as strings
Issue -
State: open - Opened by fredrik-bakke over 1 year ago
- 1 comment
Labels: bug
#155 - Re #79: Disable activating input method inside the search box
Pull Request -
State: closed - Opened by vic0103520 over 1 year ago
- 1 comment
#154 - Fix issue #76: Input method is reactivated after entering a backslash…
Pull Request -
State: closed - Opened by vic0103520 over 1 year ago
- 1 comment
#153 - Fix issue #117: Allow numeric input to complete ambiguous key bindings
Pull Request -
State: closed - Opened by vic0103520 over 1 year ago
- 1 comment
#152 - agda is running in read-only (sandboxed?) filesystem
Issue -
State: open - Opened by cspollard over 1 year ago
- 3 comments
Labels: bug
#151 - Update language configuration
Pull Request -
State: closed - Opened by fredrik-bakke over 1 year ago
- 1 comment
#150 - Fix issue #129
Pull Request -
State: open - Opened by vic0103520 over 1 year ago
Labels: dependencies
#149 - Add `wordPattern` to language-configuration.json
Issue -
State: closed - Opened by floofnoodlecode over 1 year ago
- 1 comment
#148 - Fix issue #124
Pull Request -
State: closed - Opened by lawcho over 1 year ago
- 1 comment
#147 - Bump semver from 5.7.1 to 5.7.2
Pull Request -
State: closed - Opened by dependabot[bot] over 1 year ago
- 2 comments
Labels: dependencies
#146 - v0.3.12 not available on extensions store
Issue -
State: closed - Opened by nicolo-ribaudo over 1 year ago
- 2 comments
#145 - Cannot type unicode superscript in `∧-zeroˡ`
Issue -
State: closed - Opened by uhbif19 over 1 year ago
- 2 comments
#144 - Most of the times input field for any command does not work
Issue -
State: open - Opened by uhbif19 over 1 year ago
- 4 comments
Labels: bug
#143 - Optimistic syntax highlighting
Issue -
State: open - Opened by uhbif19 over 1 year ago
Labels: enhancement
#142 - Unicode Highlight Ambiguous Characters
Issue -
State: open - Opened by fweth over 1 year ago
Labels: enhancement
#141 - Register VSCode tasks and `preLaunchTask`
Pull Request -
State: closed - Opened by fredrik-bakke almost 2 years ago
- 6 comments
#140 - Refactor conditions to enable shortcuts
Pull Request -
State: closed - Opened by pimotte almost 2 years ago
- 17 comments
#139 - No syntax highlighting?
Issue -
State: open - Opened by bzm3r almost 2 years ago
- 1 comment
Labels: unreproducible
#138 - From Agda 2.6.4: Simpler way to get Agda version using `--numeric-version` option
Issue -
State: open - Opened by andreasabel almost 2 years ago
Labels: enhancement
#137 - Building the package locally to use agda-mode input globally
Issue -
State: open - Opened by inexxt almost 2 years ago
- 1 comment
Labels: question
#136 - Bump webpack from 5.74.0 to 5.76.0
Pull Request -
State: closed - Opened by dependabot[bot] almost 2 years ago
Labels: dependencies
#135 - `editor.action.showDefinitionPreviewHover` (Hover or `Ctrl+K` type information) much slower than it should be.
Issue -
State: open - Opened by MathiasSven almost 2 years ago
Labels: bug
#133 - Bump json5 from 2.2.1 to 2.2.3
Pull Request -
State: closed - Opened by dependabot[bot] about 2 years ago
Labels: dependencies
#132 - Agda Mode Keyboard Shortcuts does not Work Except Loading a File
Issue -
State: closed - Opened by Naruyoko about 2 years ago
- 11 comments
#131 - Add "!editorHasSelection" condition to agda-mode.lookup-symbol
Issue -
State: closed - Opened by jespercockx about 2 years ago
- 1 comment
#130 - Tighten up the layout in the bottom panel.
Pull Request -
State: closed - Opened by dunhamsteve about 2 years ago
- 1 comment
#129 - Load turns editor split: left/right split into top/bottom split
Issue -
State: open - Opened by ChefYeum over 2 years ago
- 3 comments
Labels: bug
#128 - Bump loader-utils from 2.0.2 to 2.0.4
Pull Request -
State: closed - Opened by dependabot[bot] over 2 years ago
Labels: dependencies
#127 - Bump loader-utils from 2.0.2 to 2.0.3
Pull Request -
State: closed - Opened by dependabot[bot] over 2 years ago
- 1 comment
Labels: dependencies
#126 - [ fix ] Update language-server-mule to 0.2.4 (Fixes LSP)
Pull Request -
State: closed - Opened by jul1u5 over 2 years ago
- 6 comments
Labels: dependencies
#125 - Modal bindings are not shown in the goal context
Issue -
State: closed - Opened by plt-amy over 2 years ago
- 1 comment
Labels: bug
#124 - Agda files are not Markdown files
Issue -
State: closed - Opened by plt-amy over 2 years ago
- 1 comment
Labels: bug
#123 - Added logo
Pull Request -
State: closed - Opened by Trebor-Huang over 2 years ago
- 1 comment
#122 - Error starting the language server
Issue -
State: closed - Opened by damienstanton over 2 years ago
- 6 comments
Labels: bug
#121 - add lagda.md highlight support
Pull Request -
State: closed - Opened by choukh over 2 years ago
- 1 comment
#120 - Icon for agda files (and for the extension itself)
Issue -
State: closed - Opened by Trebor-Huang over 2 years ago
- 2 comments
Labels: enhancement
#119 - Customize highlighting levels
Issue -
State: open - Opened by plt-amy over 2 years ago
Labels: enhancement
#118 - Syntax highlighting for COMPILE and FOREIGN pragmas
Pull Request -
State: closed - Opened by KislyjKisel over 2 years ago
- 1 comment
#117 - Allow numeric input to complete ambiguous keyboard shortcuts
Issue -
State: open - Opened by thorimur over 2 years ago
Labels: enhancement
#116 - Agda Language Server stopped working after 0.3.10 update
Issue -
State: closed - Opened by mz71 over 2 years ago
Labels: bug
#115 - [ fix ] "go to definition" on Windows
Pull Request -
State: closed - Opened by mz71 over 2 years ago
- 1 comment
#114 - Fix typos of 'Shortcuts' in documentation
Pull Request -
State: closed - Opened by pragma- over 2 years ago
- 2 comments
#113 - Bump terser from 5.7.1 to 5.14.2
Pull Request -
State: closed - Opened by dependabot[bot] over 2 years ago
Labels: dependencies