idris-hackers/idris-mode — pull request #188 by david-christiansen (2014-06-15 21:51:43+00:00)
Title: Active terms

Active terms are regions of text that the Idris compiler has annotated with a serialized version of a term and its pretty-printing context. This means that the terms can later be manipulated without re-running the process used to create them.

For example, it is now possible to right-click a term in an error message and see the fully explicit version directly, rather than having to turn on implicits and regenerate the error. Additionally, in the metavariable list, it is possible to normalize a premise, to get a better idea of how to define the right-hand side.

Active term commands are available through keybindings and through graphical widgets.

Relies on https://github.com/idris-lang/Idris-dev/pull/1315