Completions don't work with Idris2

meraymond2 / idris-vscode

Idris front-end for VS Code

MIT License

59 stars 10 forks source link

Completions don't work with Idris2 #17

Closed meraymond2 closed 3 years ago

meraymond2 commented 3 years ago

The completions reply from the client isn't correct with Idris 2. I don't have any specific notes in the client repo about that command, but presumably the output has changed, so it no longer works.

meraymond2 commented 3 years ago

Looked at this, and the response is (:write-string "repl-completions: command not yet implemented. Hopefully soon!" 3) so that would explain why that's not working. I've just added a note to the readme that Idris2 doesn't have completions.