search

meraymond2 / idris-vscode

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

More lidr stuff #61

Closed meraymond2 closed 3 years ago

meraymond2 commented 3 years ago

This is most of the commands working. I wasn't loading lidr files correctly before, with that, you can hover over things defined in-file, and we get diagnostics too.

The main issue with lidr files is that the IDE replies are inconsistent. Warning positions are off by 2, the prefix being > (I tried without the whitespace, and it seems to be required, so at least it's consistently 2). Some of the text insertion commands work correctly, some randomly add extra arrows and or whitespace in front of the reply. :make-with is the worst, the second line starts with > > >, so there's lots of ugly prefix-fixing code. It's working on my test files, but I'm not confident that it'll work on every input. I might move some of the reply-fixing to the ide-client, where it's easier to test, but this should do for now.

meraymond2 commented 3 years ago

Commenting isn't perfect, I'd prefer > n: Nat to become > -- n: Nat, but that's not possible with VS as far as I can tell. It kinda works anyway, because it removes it from the code block.