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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and