Changes between Version 1 and Version 2 of Ticket #10


Ignore:
Timestamp:
Feb 21, 2007, 12:52:52 PM (17 years ago)
Author:
David Aspinall
Comment:

Legend:

Unmodified
Added
Removed
Modified

  • Ticket #10

    • Property Summary changed from Refactor document model out of document to Refactor and enhance document model

  • Ticket #10 – Description

    v1 v2  
    22
    33The 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.
     4
     5As 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.
     6The 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.
     7
     8A further enhancement is to add a tree of possible next commands. 
     9The tree of next commands will allow recording possible alternative steps in a proof in a lightweight (script-oriented) way.  The alternative steps may be:
     10
     11 * suggested by the user (to consider ''what if'' questions);
     12 * suggested by the prover or other component (Feasch, !IsaPlanner); or
     13 * suggested by the interface (PG Tips).
     14
     15To support this in the document we need ways of visualising the alternative branches, selecting between them, and committing them to the document. 
     16
     17The 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.
     18