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.

Sure.

Attached is an example for doing the initial startup of the session
together with the theory context; see also
https://bitbucket.org/pide/pide_examples/src/2a4cfab96b3e/ex.scala (that
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 misinterpretations:
- 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 application.

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.

Sure.

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.

Best,
Matthias





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