Determine how theorem failures should be displayed

[ericglau]

The compiler currently throws out a lot of information if theorem errors occur. Determine which parts of the theorem failure information are relevant for an IDE scenario, and how it should be presented (e.g. using diagnostic highlighting as with other errors, or something in addition to that).