Re: [isabelle] scala interface
First let's fix the Isabelle version for this thread: the latest release
Isabelle2011-1. It does not make sense to use an older Isabelle version
with Isabelle/Scala, due to the many substantial improvements of the
same that went into Isabelle2011-1.
Attached is an example for doing the initial startup of the session
together with the theory context; see also
repository might evolve further).
Thanks for this example. It clarifies the situation a lot. So new output
by the Isabelle process is announced through the commands_changed bus
and the details on the new document state can be queried with the
snapshot method. I still have difficulties understanding what kind of
information a snapshot provides.
My current view is the following; feel free to correct any
- A Document.Node is somehow the counterpart of a text buffer in jEdit.
- A Document.Snapshot is the response of the system to a Document.Node.
- The Document.Snapshot.command_state field indicates the response to a
given Isar command within the document node.
- The Command.State.results field indicates what is usually displayed in
the Output Window of jEdit.
- The Command.State.status field gives the annotations displayed with
jEdit's theory buffer.
What makes the implementation a bit delicate is the bias of Session
towards the current main application in the Isabelle/jEdit Prover IDE.
Here the user throws edits at the prover, which in turn answers them
incrementally in an fully asynchronous manner. There is never a point
where a finished execution of some command transaction is enforced. I
have recovered the latter in the above Theory_Session for the first half
of the problem: prover startup and processing the theory header.
Synchronizing input and output is one of the main challenges in my
What is still missing in the above ex.scala is the part about emitting
the statement and proof, and inspecting its results. This requires some
extra care due to potential non-termination of that part of the document.
We can discuss in further detail what your application really requires.
There is much more to say and I would appreciate to discuss this, but I
have a deadline for next weekend. I will come back to you after this.
This archive was generated by a fusion of
Pipermail (Mailman edition) and