src/Pure/PIDE/document.ML
changeset 38363 af7f41a8a0a8
parent 38355 8cb265fb12fe
child 38373 e8197eea3cd0
equal deleted inserted replaced
38362:754ad6340055 38363:af7f41a8a0a8
     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 = int
    10   type id = int
    11   type command_id = int
    11   type exec_id = id
    12   type version_id = int
    12   type command_id = id
    13   val no_id: int
    13   type version_id = id
    14   val parse_id: string -> int
    14   val no_id: id
    15   val print_id: int -> string
    15   val parse_id: string -> id
       
    16   val print_id: id -> string
    16   type edit = string * ((command_id * command_id option) list) option
    17   type edit = string * ((command_id * command_id option) list) option
    17 end;
    18 end;
    18 
    19 
    19 structure Document: DOCUMENT =
    20 structure Document: DOCUMENT =
    20 struct
    21 struct
    21 
    22 
    22 (* unique identifiers *)
    23 (* unique identifiers *)
    23 
    24 
    24 type state_id = int;
    25 type id = int;
    25 type command_id = int;
    26 type exec_id = id;
    26 type version_id = int;
    27 type command_id = id;
       
    28 type version_id = id;
    27 
    29 
    28 val no_id = 0;
    30 val no_id = 0;
    29 
    31 
    30 fun parse_id s =
    32 fun parse_id s =
    31   (case Int.fromString s of
    33   (case Int.fromString s of