Re: [isabelle] Message output in Isabelle2014 and Isabelle2015



> On a multi-window GUI there is no point to squeeze everything into a 
> single linear output.  The Query panel already provides a different way to 
> view a proof state, independently on Output.  Such things are relatively 
> easy to make, and don't require artificial intelligence from the system to 
> guess what the user wants to see.

So we could extract two feature requests:
  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.

  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.


--
  Peter








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