Re: [isabelle] scala interface
On Mon, 20 Feb 2012, Matthias Schmalz wrote:
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
Document.Node identifies each document node in a semi-abstract manner.
It is indeed modeled after editor text buffers, can be used in other ways
as well. In the example, I've identified the fresh theory node by some
something like /dummy-42/Theory.thy
Document.Snapshot is the main access point of the totality of a collection
of document nodes in a document version, with semantic markup attached
(via the internal Command.State components). This is the main programming
interface to access results. It provides a defined point in space and
time of the ongoing process of continous checking of the sources. The key
operation is Snapshot.select_markup, but in the present example I have
uses more low-level status and results fields from individual command
Command.State.results and Command.State.status are special cases of the
primary "markup" component of accumulated state information. In fact,
after Isabelle2011-1 the focus is shifting further to that general markup
tree, and result messages and status information might have to be
retrieved via Snapshot.select and some further variants of it.
This archive was generated by a fusion of
Pipermail (Mailman edition) and