Comments (1)
I think the only relevant thing is that the List Metavariables
command was broken, but it's been subsequently fixed. If you're building from the main branch, it'll be fine, but with the 0.5.0 release, the command won't do anything do to a JS exception.
Since it doesnโt break the whole plugin, just that one command, I'm inclined to just wait for it to be fixed in the next release, rather than implement a workaround specifically for 0.5.0, because that would break it for anyone using a previous or later version.
from idris-vscode.
Related Issues (20)
- open-vsx support HOT 3
- Explain how to install this HOT 4
- ERR_STREAM_DESTROYED when trying to run command `idris.addClause` HOT 8
- Syntax highlighting sometimes fails HOT 3
- show type not working in .lidr file HOT 9
- Support v0.4.0 HOT 2
- Hovering over contents of a new takes about one minute HOT 8
- file path is wrong within workspace with multiple folders HOT 4
- Is it possible to get hole type with just keyboard, not with mouse hover? HOT 2
- What do you think of idris2-lsp-vscode? HOT 4
- Feature request: Jump to definition, Ctrl-Click. HOT 4
- "Idris 2 mode" checkbox is missing HOT 1
- Failed to load file. HOT 2
- Error display in wrong line: always 1 line upper HOT 8
- How to configure packages? HOT 10
- Publish 0.0.14 to Open VSX HOT 1
- Having issue with extension HOT 4
- Activate extension on language 'idris2' too HOT 6
- Add Missing is not working
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
๐ Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. ๐๐๐
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google โค๏ธ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from idris-vscode.