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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and