src/Pure/PIDE/document.ML
author wenzelm
Wed Aug 11 22:41:26 2010 +0200 (2010-08-11)
changeset 38355 8cb265fb12fe
parent 38150 67fc24df3721
child 38363 af7f41a8a0a8
permissions -rw-r--r--
represent document ids by (long) int, to benefit from the somewhat faster Inttab in ML (LinearSet in Scala is invariably indexed by native object ids);
     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 = int
    11   type command_id = int
    12   type version_id = int
    13   val no_id: int
    14   val parse_id: string -> int
    15   val print_id: int -> string
    16   type edit = string * ((command_id * command_id option) list) option
    17 end;
    18 
    19 structure Document: DOCUMENT =
    20 struct
    21 
    22 (* unique identifiers *)
    23 
    24 type state_id = int;
    25 type command_id = int;
    26 type version_id = int;
    27 
    28 val no_id = 0;
    29 
    30 fun parse_id s =
    31   (case Int.fromString s of
    32     SOME i => i
    33   | NONE => raise Fail ("Bad id: " ^ quote s));
    34 
    35 val print_id = signed_string_of_int;
    36 
    37 
    38 (* edits *)
    39 
    40 type edit =
    41   string *  (*node name*)
    42   ((command_id * command_id option) list) option;  (*NONE: remove, SOME: insert/remove commands*)
    43 
    44 end;
    45