idris-lang/Idris-dev — pull request #1315 by david-christiansen (2014-06-15 21:38:27+00:00)
Title: Serialize original TT terms, and annotate pretty-printer output

This allows IDEs to do things like request fully-explicit versions or normalised versions of eg terms that occur in error messages and proof contexts