Re: [isabelle] Isabelle2011 jEdit



On Wed, 16 Feb 2011, Brian Huffman wrote:

Generating files at run-time confuses the Isabelle theory loader even now, and this is becoming more restrictive when multiple versions are managed by the system simultaneously.

How does Isabelle's code generator (e.g. for Haskell) fit in with this new document model?

As long as generated files are not considered part of the running session, this should work.

Another possibility is to generate that Haskell code in a value-oriented way and pass it to a suitable external process an the spot. In practice this means to generate "anonymous" temp files that do not persist. There are already tools that work like that.

Yet another scenario is that some tool generates sources for inclusion into the edited document, but this means it refers to a newer "version" of the same, without any mutation.


	Makarius





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.