src/Pure/PIDE/document.ML
changeset 38150 67fc24df3721
child 38355 8cb265fb12fe
equal deleted inserted replaced
38149:3c380380beac 38150:67fc24df3721
       
     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