Refactor and enhance document model

[anonymous]

Refactor ProofScriptDocument to remove the document model explicitly as ProofScriptModel.

The document model should be a parse tree of the document (perhaps with whitespace elements re-added), which we can easily extend with meta information about element status. The document class should offer a presentation of this model.

As a second stage after refactoring, we can enhance the script model to match the PGIP document model to allow meta data and even fragments from other documents to allow literate-style development. The script model then becomes richer than the actual script document; we may want to persisting the extra data as meta data or hidden files in the workspace.

A further enhancement is to add a tree of possible next commands. The tree of next commands will allow recording possible alternative steps in a proof in a lightweight (script-oriented) way. The alternative steps may be:

• suggested by the user (to consider what if questions);
• suggested by the prover or other component (Feasch, IsaPlanner); or
• suggested by the interface (PG Tips).

To support this in the document we need ways of visualising the alternative branches, selecting between them, and committing them to the document.

The more advanced possibilities above need careful design and refinement of the broker design and PGIP document model. Our MKM 2005 paper has steps in this direction. The PGIP document model should match the ProofScriptModel in Eclipse rather closely, except that the model in Eclipse may contain extra information relating to the state in the interface.

[David Aspinall]

Milestone PG-Eclipse-1.1.0 deleted