idris-lang/Idris-dev — pull request #1655 by david-christiansen (2014-10-18 06:16:09+00:00)
Title: Retain parser and type errors in documentation code samples

This PR adds support for retaining error messages encountered when parsing and elaborating code samples that are indicated as Idris code. It also reports these error objects to IDE clients.

There's no support for showing them in the console due to my inability to find a reasonable interface in the limited collection of available colors and styles, as well as the clunky API.

Also, @johnny-john's code examples in List all type check now, which makes them display as intended.