Re: [isabelle] Message output in Isabelle2014 and Isabelle2015



On Tue, 23 Jun 2015, Peter Lammich wrote:

 1. Allow for a separate errors/warnings and a proof state panel.
Ensure that they can be laid out nicely, such that the user can view
them both simultaneously. In current jedit, the panels could be detached
and the layout been done by the OSs' window manager.

That is relatively simple, as I have pointed out already.

I can immediately imagine further improvements, but it will require to move further and faster beyond old customs, and that has often been inhibited in the past few years.


 2. Change the current output/proof state panel to display (short
versions of) error messages before warnings. The errors displayed on the
squiggly lines may of course still contain the proof state. I know that
this may be a technical problem, b/c (as far as I know) error messages
are generated by the ML-side, and not touched by the IDE.

That is the "AI" approach to messages again. It has already been disproven many times in the past.

Errors and warnings need to be produced and managed as uniformly as possible. Special treatment and variations tend to cause unexpected breakdown. We've had that e.g. in the goal state output in tactic failure when it was first introduced, and only shortly after the release back then you discovered that the goal was printed without the flags of normal goal state printing, causing denial-of-service in the front-end for big states.


	Makarius




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.