src/Pure/PIDE/document.ML
author wenzelm
Sat Aug 14 11:52:24 2010 +0200 (2010-08-14 ago)
changeset 38373 e8197eea3cd0
parent 38363 af7f41a8a0a8
child 38414 49f1f657adc2
permissions -rw-r--r--
tuned;
     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 id = int
    11   type version_id = id
    12   type command_id = id
    13   type exec_id = id
    14   val no_id: id
    15   val parse_id: string -> id
    16   val print_id: id -> string
    17   type edit = string * ((command_id * command_id option) list) option
    18 end;
    19 
    20 structure Document: DOCUMENT =
    21 struct
    22 
    23 (* unique identifiers *)
    24 
    25 type id = int;
    26 type version_id = id;
    27 type command_id = id;
    28 type exec_id = id;
    29 
    30 val no_id = 0;
    31 
    32 fun parse_id s =
    33   (case Int.fromString s of
    34     SOME i => i
    35   | NONE => raise Fail ("Bad id: " ^ quote s));
    36 
    37 val print_id = signed_string_of_int;
    38 
    39 
    40 (* edits *)
    41 
    42 type edit =
    43   string *  (*node name*)
    44   ((command_id * command_id option) list) option;  (*NONE: remove, SOME: insert/remove commands*)
    45 
    46 end;
    47