[isabelle-dev] Diagnostic commands in jedit?

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Fri Sep 30 13:31:13 CEST 2011

> 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.)




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://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20110930/6a3e3f12/attachment.sig>

More information about the isabelle-dev mailing list