search

idris-hackers / idris-mode

Idris syntax highlighting, compiler-supported editing, interactive REPL and more things for Emacs.
GNU General Public License v3.0
268 stars 70 forks source link

Support the Idris 2 proof-search-next IDE protocol command #511

Closed scotek closed 3 years ago

scotek commented 4 years ago

Idris 2 provides a new protocol command (proof-search-next) to iterate through multiple attempts to solve a hole. This was raised in issue #510 .

The first commit in this branch adds support for the new command. The second commit works around issue #509 which stops the basic proof-search command from working in Idris 2. It will still work in Idris 1 but without the optional arguments functionality.

The code passes the tests if the unused variables left over from the 509 fix above are taken out but given that is only a workaround you might prefer if they were left in?

jfdm commented 3 years ago

I am very sorry that this PR has been the 'p' and 'r' in purgatory. Having started on some revision of the mode to accommodate breaking changes to the IDE protocol in Idris2, I saw that I missed the follow up to this. I've addressed merge conflicts and merged now. Very sorry about this.