search

meraymond2 / idris-vscode

Idris front-end for VS Code
MIT License
58 stars 10 forks source link

show type not working in .lidr file #53

Closed joelberkeley closed 2 years ago

joelberkeley commented 3 years ago

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.

meraymond2 commented 3 years ago

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.

joelberkeley commented 3 years ago

that'd be really great

meraymond2 commented 3 years ago

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?

joelberkeley commented 3 years ago

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.

meraymond2 commented 3 years ago

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.

joelberkeley commented 3 years ago

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.

joelberkeley commented 3 years ago

looks like agda uses

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

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

meraymond2 commented 3 years ago

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.

meraymond2 commented 2 years ago

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.