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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
