New ML antiquotation 'code': takes constant as argument, generates
corresponding code in background and inserts name of the corresponding
resulting ML value/function/datatype constructor binding in place. All
occurences of 'code' with a single ML block are generated simultaneously.
Provides a generic and safe interface for instrumentalizing code
generation. See HOL/ex/Code_Antiq for a toy example, or
HOL/Complex/ex/ReflectedFerrack for a more ambitious application. In
future you ought refrain from ad-hoc compiling generated SML code on
the ML toplevel.
Note that (for technical reasons) 'code' cannot refer to constants for
which user-defined serializations are set. Refer to the corresponding
ML counterpart directly in that cases.
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: 252 bytes
Desc: OpenPGP digital signature
Url :
https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20080702/07ee4551/attachment.pgp
