show type not working in .lidr file about idris-vscode HOT 9 CLOSED

That could work, I'll have to look at how they do it. I mainly want to avoid this extension starting up every time you open a readme, but I think naming a file .lidr.md would be solve that.

I've made a release with the .lidr improvements I've done so far — I didn't want to wait any longer to get the 0.4.0 fix out. But I'll work on the other files types for the next one.

from idris-vscode.

Hi,

at the moment, the extension does almost nothing for .lidr files, just some syntax-highlighting. I can look at activating the type-checking and hovering for .lidr files too though.

from idris-vscode.

that'd be really great

from idris-vscode.

I've got a fix for the hover done. I'll try and make a new release soon, I'm going to see if I can squeeze it in with the 0.4.0 support.

For .lidr files, I've only specifically added code to get the hover to work. Auto complete seems to be working, error highlighting isn't. The commands that insert text are probably all broken — I may just disable those for .lidr files for now rather than have them do weird things.

I don't know how much work it'll be to get all of the commands working, but are there any functions besides hovering that you would really like implemented for the next release?

from idris-vscode.

what you've done is really helpful already, thanks. Just whenever you have time. In terms of what would be most helpful, error highlighting would be great. I'm also exploring the alternative formats: .md, .tex and there's one other I can't remember the name of. If they're easy to add & maintain, they'd also be great.

from idris-vscode.

I've got most of the commands working now, and error highlighting.

I don't think it's going to be possible to get any of the extension features for markdown, latex or org mode, because the extension is activated per file, so .lidr works ok, because no other extension is trying to handle them. I might be able to provide syntax highlighting, at least for the built-in markdown plugin, but nothing like hover, or error handling.

An aside: is it weird that the normal text in the .lidr file is syntax-highlighted as comments? I borrowed the syntax grammar, indirectly, from the original Atom plugin and didn't really think about it, but now I'm concerned that the normal text isn't readable. With my colour theme at least, the comment colour is grey on grey. I'd imagine that a literate Idris file is going to be more text than code, otherwise one would just use actual comments.

from idris-vscode.

That's great.

Re .md files, I take it that's a vscode limitation, not being able to enable extensions for parts of files?

Makes sense to me to syntax-highlight the normal text as comments. It's green in my editor, and perfectly readable. I guess no highlighting is another option but I don't think there's any need to change it.

from idris-vscode.

looks like agda uses

.agda
.lagda
.lagda.md
.lagda.tex
.lagda.rst

would that work for idris e.g. .lidr.md?

from idris-vscode.

The markdown support is released now, in 0.0.11.

I can leave this issue open a bit longer for latex or org mode support, which I haven't implemented. I don't use either of those, but if anyone wants support for them and can provide an example file, I'll have a go at it.

from idris-vscode.