[isabelle-dev] user errors

[Christian Sternagel]

Maybe this is for Florian or Lukas,

Routinely checking all the TODOs and FIXMEs in our IsaFoR sources I 
found the following fragment:

   subsection {* User exceptions in generated code *}
   (* FIXME:  will be moved to Main. update: did not happen for 
Isabelle2012. *)

   definition error :: "String.literal => 'a => 'a"
   where [code del]: "error msg x = x"

   code_const error
     (Eval "(fn msg =>/ fn x =>/ error msg)")

   code_reserved Eval error

Would it make sense to make this part of Main as indicated in the comment?

cheers

chris