src/Pure/PIDE/document.ML
changeset 38373 e8197eea3cd0
parent 38363 af7f41a8a0a8
child 38414 49f1f657adc2
     1.1 --- a/src/Pure/PIDE/document.ML	Fri Aug 13 21:33:13 2010 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Sat Aug 14 11:52:24 2010 +0200
     1.3 @@ -8,9 +8,9 @@
     1.4  signature DOCUMENT =
     1.5  sig
     1.6    type id = int
     1.7 -  type exec_id = id
     1.8 +  type version_id = id
     1.9    type command_id = id
    1.10 -  type version_id = id
    1.11 +  type exec_id = id
    1.12    val no_id: id
    1.13    val parse_id: string -> id
    1.14    val print_id: id -> string
    1.15 @@ -23,9 +23,9 @@
    1.16  (* unique identifiers *)
    1.17  
    1.18  type id = int;
    1.19 -type exec_id = id;
    1.20 +type version_id = id;
    1.21  type command_id = id;
    1.22 -type version_id = id;
    1.23 +type exec_id = id;
    1.24  
    1.25  val no_id = 0;
    1.26