[isabelle-dev] Errors in right bar shadowed by warnings

[Makarius]

On Thu, 15 May 2014, Lars Noschinski wrote:

> A video (slightly bad quality, the state of options to do simple video
> cropping in Linux seems kind of ... bad):
>
>   http://www21.in.tum.de/~noschinl/isabelle-shadowed-errors.m4v

Thanks for the video.  It is always fun to watch the system running, and 
it often gives the right idea rather quickly, without too much digging in 
the sources, side-conditions of the situation etc.

The result after some bisection of the history is this rather trivial 
changeset:

changeset:   56980:9c5220e05e04
tag:         tip
user:        wenzelm
date:        Fri May 16 17:11:56 2014 +0200
summary:     proper priority for error over warning, which got mixed up in 
0546e036d1c0 and 4df2727a0b5f;


There is a long story behind the "command status" question, and it is 
hardly settled now.  In 2006/2007 we've had some discussions with David 
Aspinall for the propective PGIP protocol, for the time after Proof 
General, which was supposed to be ended in 2008 already.

The only conclusion from it is that the status cannot be defined once and 
for all, for all provers and all time.


 	Makarius