idris-hackers/idris-mode — pull request #178 by david-christiansen (2014-06-08 02:19:32+00:00)
Title: Make the prover work

This pull request relies on a few backwards-incompatible changes to Idris, thus it's after the 0.9.13 tag.
In particular, it needs https://github.com/idris-lang/Idris-dev/pull/1296.

New features/bug fixes:
* When you complete a proof, Idris asks if you want to add it. If you say yes, it works like :addproof.
* Semicolons are no longer used in proof script buffers
* Keybinding in script buffers is M-n, M-p to work like REPL history
* RET works in proof script buffers even if is next to read-only characters
* Abandoning proofs no longer desynchronizes Idris
* The prover remembers your window config and restores it after proving
* The metavariable list contains buttons to launch the prover
* Right-clicking metavar names in Idris output gives a menu that includes launching the prover
* More functions and variables have doc
* The event log buffer contains readable timestamps for easier debugging