Re: [isabelle] 2014-RC1 issues
On Fri, 1 Aug 2014, Lars Noschinski wrote:
An issue with the precedence of warnings and errors:
Under certain circumstances, if a method emits a warning and the apply
fails (with an error), the line is only marked as a warning in the
theories panel and the right side bar.
It should we OK in the right side bar -- according to
http://www.mail-archive.com/isabelle-dev at mailbroy.informatik.tu-muenchen.de/msg05328.html
from May 2014. Back then I somehow forgot to apply the analogous change to
the theories panel as well.
My comment from that thread on isabelle-dev about the difficulty to pin
down the notion of "command status" still applies: the Prover IDE merely
visualizes certain aspects of very rich information; sometimes it might
come out in a misleading way.
This archive was generated by a fusion of
Pipermail (Mailman edition) and