> Things like code generation might be of the form of associating document > content that is generated by functional evaluation over the semantics of > the formal source text. Think of it as part of browser_info, not the > src tree. Part of the question is who or what is the target of > generated sources. One might consider funny ways to refer to > "resources" of a theory node, similar to the way 'uses' are located now > within the file-system wrt. the master directory, but without an actual > physical directory.
I was actually thinking in a similar direction. So a first step would
be to come up with an idea how to integrate document preparation into
the IDE-style user interaction of Isabelle/jedit without the current
low-level tinkering we are doing at the moment (batch sessions,
makefiles, arcane ROOT files etc.)
Florian
--
Home:
http://www.in.tum.de/~haftmann
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
