Re: [isabelle] Message output in Isabelle2014 and Isabelle2015

> > The deeper problem is cluttering of Output with too many different things, 
> > and the lack of a dedicated panel just for proof state output. 
> For those people with large screens, this may be a good solution. It
> already worked nicely for PG, where I usually used the "3-pane" mode, or
> had three windows: Text, Goal-state, Errors/Warnings. 
> To make up for a nice layout, I would like to dock one panel to
> right-top, and the other to right-bottom. Does jedit support such
> docking positions, that go beyond left,right,top,bottom?
> If you work on a small screen (laptop), you probably still want to have
> a mode that consumes less space, and sensibly mixes the outputs.
> However, I do not know how a PIDE-like asynchronous IDE can guess what
> the user currently wants to see. Perhaps, you could try a heuristics on
> the type of error, something like: 
> Syntax-errors are displayed after the goal-state, failed method errors
> before the goal-state.

One solution that does not involve too much implementation effort might
be to not include the goal-state into the error message, and output this
shorter error message *before* the goal-state. 

While the user is typing, he would see a short error message that he
could ignore, followed by the goal state. 
When the user is inspecting the (error-)result of the command, he would
see the error message first. Warnings should still be printed after the


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