Re: [isabelle] 2014-RC1 issues
On Wed, 30 Jul 2014, Lars Noschinski wrote:
On 30.07.2014 10:26, Peter Lammich wrote:
Here is a list of issues that I encountered with RC1:
And yet another issue: A method executing
produces an error marker in the right sidebar. However, the associated
apply command does not get underlined in red and the error marker in the
left sidebar is missing.
That is an interesting boundary case, but it is the same in
Isabelle2013-2 an no regression. It remains to be seen if it is an actual
The invocation of error "" is the same as raise ERROR "", which makes the
ML code fail and the Isar toplevel wrapper print the exeptions. The error
message is empty, which means it is vacous according to ancient Isabelle
traditions, which hold until today. The effect was not visible in the old
TTY times, because that adds a prefix of "*** " by default. Note that
there are other situations where ML failure might lead to no error output,
notably involving Exn.Interrupt.
Such non-printing exceptions should not show up under normal circumstances
-- they indicate a programming mistake somewhere.
The "implementation" manual explains the difference of user ERROR vs.
system Fail exceptions explicitly. The error function / ERROR exception
always had the implicit assumption that messages are non-empty, as a
proper human-readable message.
For your application of a meaningless ad-hoc failure, you could raise
Fail "" or even raise Match (which are both printed as usual). The
"undefined" function also does the latter.
This archive was generated by a fusion of
Pipermail (Mailman edition) and