Re: [isabelle] 2014-RC1 issues

On 30.07.2014 13:49, Ondřej Kunčar wrote:
> And you can't see the error in the Output panel either.
Indeed. All of this is different to

  ML {* error "" *}

which at least produces an empty red line as output (and thus gets the
other markers, too).

BTW: I always use(d) "error """ the way one uses "undefined" in Haskell.
The following construct (which Makarius showed me at ITP) is a bit nicer
(you get a trace and can jump to the location of the error), but
requires a few lines of initial setup:

signature UTIL = sig
  exception Undefined
  val setup : theory -> theory

structure Util : UTIL = struct

exception Undefined

val setup =
  ML_Antiquotation.inline @{binding undef} (Scan.succeed "raise
  #> ML_Antiquotation.inline @{binding fundef} (Scan.succeed "fn _ =>
raise Util.Undefined")


BTW2: I assume there is no easy way to make Isabelle/ML accept ⊥ instead
of @{undef}?

  -- Lars

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