[isabelle-dev] user errors

[Florian Haftmann]

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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 259 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20121031/23f7deee/attachment.sig>