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.


	Makarius





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