show type not working in .lidr file
joelberkeley opened this issue · 9 comments
I'm not seeing any "show type" information in a Foo.lidr with contents
> foo : Integer
> foo = ?fooRhs
when I hover over ?fooRhs. I do see it for the corresponding .idr code.
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.
that'd be really great
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?
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.
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.
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.
looks like agda uses
.agda
.lagda
.lagda.md
.lagda.tex
.lagda.rst
would that work for idris e.g. .lidr.md?
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.
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.