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 () =>