src/Pure/PIDE/document.ML
changeset 38363 af7f41a8a0a8
parent 38355 8cb265fb12fe
child 38373 e8197eea3cd0
     1.1 --- a/src/Pure/PIDE/document.ML	Thu Aug 12 14:22:23 2010 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Thu Aug 12 15:19:11 2010 +0200
     1.3 @@ -7,12 +7,13 @@
     1.4  
     1.5  signature DOCUMENT =
     1.6  sig
     1.7 -  type state_id = int
     1.8 -  type command_id = int
     1.9 -  type version_id = int
    1.10 -  val no_id: int
    1.11 -  val parse_id: string -> int
    1.12 -  val print_id: int -> string
    1.13 +  type id = int
    1.14 +  type exec_id = id
    1.15 +  type command_id = id
    1.16 +  type version_id = id
    1.17 +  val no_id: id
    1.18 +  val parse_id: string -> id
    1.19 +  val print_id: id -> string
    1.20    type edit = string * ((command_id * command_id option) list) option
    1.21  end;
    1.22  
    1.23 @@ -21,9 +22,10 @@
    1.24  
    1.25  (* unique identifiers *)
    1.26  
    1.27 -type state_id = int;
    1.28 -type command_id = int;
    1.29 -type version_id = int;
    1.30 +type id = int;
    1.31 +type exec_id = id;
    1.32 +type command_id = id;
    1.33 +type version_id = id;
    1.34  
    1.35  val no_id = 0;
    1.36