[isabelle-dev] isabelle build and code generation

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Wed Aug 8 21:20:09 CEST 2012

I wonder whether there is a possibility to generalize the session
concept to other generates beyond tex as well, in particular generated
code, e.g.

session Foo = HOL +
    Bar [export_code = blubb in SML]

This would subsume the rather arcane »isabelle codegen«, and give the
existing export_code a similar status like display_draft or thy_deps
(and to all of them, hopefully, a more reasonable interaction paradigm
than the current side effects on reparsing in jEdit).

The key question is whether it is worth to overstrap the concept of
options that far.



PGP available:

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 262 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20120808/dce77256/attachment.asc>

More information about the isabelle-dev mailing list