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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
