edwinb/Idris-dev — pull request #17 by dpmulligan (2012-03-01 13:29:39+00:00)
Title: Improved pretty printing support for proof states

Improved pretty printing support for proof states. Much better at displaying large goals, especially. Moved away from using Show type class to using a custom Pretty type class based around the HughesPJ pretty printing library, along with a "size" calculation for any type that is pretty printed, in order to calculate when a line should be broken.

Tested on some large goals from trying to prove the heap implementation correct, and also smaller goals from the Nat.idr file in the Prelude. Everything looks OK, but some bugs may be hiding due to a lack of test coverage.