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
end

structure Util : UTIL = struct

exception Undefined

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

end

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.