Comments (4)
It's cool. My assumption is that it will replace this extension when the language server catches up. I haven't been following the progress of the language server recently, but the last time I looked there was still quite a bit to do, I need to check on it again. Possibly the two can complement each other in the meantime.
I haven't looked at the semantic highlighting for source in a while, I remember it was a bit problematic. The IDE Protocol only works with files on disk. It's easy to do the initial highlighting but not easy to keep it updated when you start typing.
Off the top of my head I could
- highlight on load, and drop it all again once the user starts typing until they save again
- save the file on every change
- highlight on load, try to shift it along as edits are made, and re-highlight on save
- copy the source file to a temporary file, which could be saved on each edit
but I didn't like any of those options. I'm guessing the language server is keeping it in memory and re-parsing on each update.
from idris-vscode.
I won't recommend using both extensions at the same time. Unfortunately even the Idris API doesn't support working with unsaved files. The server relies on the client (VSCode) to shift the highlights as edits are made.
from idris-vscode.
It supports semantic highlighting of Idris source files.
Do you mean that extension supports semantic highlighting already, or just that the Language Server does?
I'm thinking about taking another stab at this. It wasn't a priority before because the v2 ide-mode wasn't sending the semantic metadata, but it is now for most messages, so it could be worth doing.
from idris-vscode.
VSCode supports semantic tokens and so does the language server. The extension is fairly minimal and just connects VSCode to the language server. To support features not covered by the LSP spec the code would have to be added to the extension. When the client asks for semantic tokens about a document that is different than is on disk, the server sends RequestCancelled
which is a bit of a hack. The server triggers a reload of all semantic tokens when a file is saved. VSCode intelligently moves the semantic tokens in between. Why not just switch to the LSP?
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
- Version 0.5.0 HOT 1
- 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
- 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.