idris-hackers/idris-mode — pull request #155 by david-christiansen (2014-05-22 20:29:08+00:00)
Title: Load region

This allows a ProofGeneral style of interaction in Idris buffers. Now, when C-c C-l is given a prefix argument, it loads up to the definition that point is on. A background color is used to show the currently-loaded part of the buffer. C-c C-n and C-c C-p allow moving the marker for how much to load up and down. Interactive editing commands automatically extend the loaded region just enough to encompass where the command will be applied.

Relies on https://github.com/idris-lang/Idris-dev/pull/1253, which also changes the protocol slightly. Now, when a file is loaded, instead of returning a string that states this, it returns an FC stating the maximum position that was loaded.