[isabelle-dev] isabelle build and code generation

[Florian Haftmann]

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 +
  theories
    …
  theories
    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.

	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: 262 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20120808/dce77256/attachment.asc>