1.1 --- a/src/Pure/PIDE/document.ML	Sun Aug 15 18:41:23 2010 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Sun Aug 15 19:30:11 2010 +0200
     1.3 @@ -12,7 +12,7 @@
     1.4    type command_id = id
     1.5    type exec_id = id
     1.6    val no_id: id
     1.7 -  val create_id: unit -> id
     1.8 +  val new_id: unit -> id
     1.9    val parse_id: string -> id
    1.10    val print_id: id -> string
    1.11    type edit = string * ((command_id * command_id option) list) option
    1.12 @@ -38,7 +38,7 @@
    1.13  local
    1.14    val id_count = Synchronized.var "id" 0;
    1.15  in
    1.16 -  fun create_id () =
    1.17 +  fun new_id () =
    1.18      Synchronized.change_result id_count
    1.19        (fn i =>
    1.20          let val i' = i + 1
    1.21 @@ -243,7 +243,7 @@
    1.22  fun new_exec name (id: command_id) (exec_id, updates, state) =
    1.23    let
    1.24      val exec = the_exec state exec_id;
    1.25 -    val exec_id' = create_id ();
    1.26 +    val exec_id' = new_id ();
    1.27      val tr = Toplevel.put_id (print_id exec_id') (the_command state id);
    1.28      val exec' =
    1.29        Lazy.lazy (fn () =>