Hi Christian
> 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?
In principle yes. For sake of quality it should then be operative also
for vanilla SML, OCaml, Haskell and Scala.
Cheers,
Florian
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
