Re: [isabelle] scala interface



On Mon, 20 Feb 2012, Matthias Schmalz wrote:

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.

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 states.

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.


	Makarius





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