src/Pure/PIDE/document.ML
changeset 38373 e8197eea3cd0
parent 38363 af7f41a8a0a8
child 38414 49f1f657adc2
equal deleted inserted replaced
38372:e753f71b6b34 38373:e8197eea3cd0
     6 *)
     6 *)
     7 
     7 
     8 signature DOCUMENT =
     8 signature DOCUMENT =
     9 sig
     9 sig
    10   type id = int
    10   type id = int
       
    11   type version_id = id
       
    12   type command_id = id
    11   type exec_id = id
    13   type exec_id = id
    12   type command_id = id
       
    13   type version_id = id
       
    14   val no_id: id
    14   val no_id: id
    15   val parse_id: string -> id
    15   val parse_id: string -> id
    16   val print_id: id -> string
    16   val print_id: id -> string
    17   type edit = string * ((command_id * command_id option) list) option
    17   type edit = string * ((command_id * command_id option) list) option
    18 end;
    18 end;
    21 struct
    21 struct
    22 
    22 
    23 (* unique identifiers *)
    23 (* unique identifiers *)
    24 
    24 
    25 type id = int;
    25 type id = int;
       
    26 type version_id = id;
       
    27 type command_id = id;
    26 type exec_id = id;
    28 type exec_id = id;
    27 type command_id = id;
       
    28 type version_id = id;
       
    29 
    29 
    30 val no_id = 0;
    30 val no_id = 0;
    31 
    31 
    32 fun parse_id s =
    32 fun parse_id s =
    33   (case Int.fromString s of
    33   (case Int.fromString s of