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

  error ""

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 problem.

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 MHonArc.