[isabelle-dev] Errors in right bar shadowed by warnings
makarius at sketis.net
Fri May 16 17:40:48 CEST 2014
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):
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
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.
More information about the isabelle-dev