src/Pure/PIDE/document.ML
author wenzelm
Thu Aug 05 14:35:35 2010 +0200 (2010-08-05 ago)
changeset 38150 67fc24df3721
child 38355 8cb265fb12fe
permissions -rw-r--r--
simplified/refined document model: collection of named nodes, without proper dependencies yet;
moved basic type definitions for ids and edits from Isar_Document to Document;
removed begin_document/end_document for now -- nodes emerge via edits;
edits refer to named nodes explicitly;
     1 (*  Title:      Pure/PIDE/document.ML
     2     Author:     Makarius
     3 
     4 Document as collection of named nodes, each consisting of an editable
     5 list of commands.
     6 *)
     7 
     8 signature DOCUMENT =
     9 sig
    10   type state_id = string
    11   type command_id = string
    12   type version_id = string
    13   val no_id: string
    14   type edit = string * ((command_id * command_id option) list) option
    15 end;
    16 
    17 structure Document: DOCUMENT =
    18 struct
    19 
    20 (* unique identifiers *)
    21 
    22 type state_id = string;
    23 type command_id = string;
    24 type version_id = string;
    25 
    26 val no_id = "";
    27 
    28 
    29 (* edits *)
    30 
    31 type edit =
    32   string *  (*node name*)
    33   ((command_id * command_id option) list) option;  (*NONE: remove, SOME: insert/remove commands*)
    34 
    35 end;
    36