src/Pure/PIDE/document.ML
changeset 38355 8cb265fb12fe
parent 38150 67fc24df3721
child 38363 af7f41a8a0a8
equal deleted inserted replaced
38354:fed4e71a8c0f 38355:8cb265fb12fe
     5 list of commands.
     5 list of commands.
     6 *)
     6 *)
     7 
     7 
     8 signature DOCUMENT =
     8 signature DOCUMENT =
     9 sig
     9 sig
    10   type state_id = string
    10   type state_id = int
    11   type command_id = string
    11   type command_id = int
    12   type version_id = string
    12   type version_id = int
    13   val no_id: string
    13   val no_id: int
       
    14   val parse_id: string -> int
       
    15   val print_id: int -> string
    14   type edit = string * ((command_id * command_id option) list) option
    16   type edit = string * ((command_id * command_id option) list) option
    15 end;
    17 end;
    16 
    18 
    17 structure Document: DOCUMENT =
    19 structure Document: DOCUMENT =
    18 struct
    20 struct
    19 
    21 
    20 (* unique identifiers *)
    22 (* unique identifiers *)
    21 
    23 
    22 type state_id = string;
    24 type state_id = int;
    23 type command_id = string;
    25 type command_id = int;
    24 type version_id = string;
    26 type version_id = int;
    25 
    27 
    26 val no_id = "";
    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;
    27 
    36 
    28 
    37 
    29 (* edits *)
    38 (* edits *)
    30 
    39 
    31 type edit =
    40 type edit =