idris-hackers/idris-mode — pull request #260 by david-christiansen (2014-10-18 06:28:48+00:00)
Title: Support displaying embedded errors in docstrings

See https://github.com/idris-lang/Idris-dev/pull/1655