Re: [isabelle] Isabelle2011 jEdit



On Wed, Feb 16, 2011 at 11:28 AM, Makarius <makarius at sketis.net> wrote:
> On Wed, 16 Feb 2011, Lucas Dixon wrote:
>> I do some fairly non-standard things with Isabelle... saving files as side
>> effects of processing, opening new pipes to/from isabelle, etc, etc.
>
> That's a more fundamental problem.  The main idea behind the new document
> model is that it is stateless and timeless, so there are by definition no
> side-effects.
>
> 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?

- Brian





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