diff -r 38c5b085fb1c -r bb42bc831570 src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Fri Aug 26 15:56:30 2011 +0200
+++ b/src/Pure/PIDE/document.ML	Fri Aug 26 16:06:58 2011 +0200
@@ -28,7 +28,7 @@
   val join_commands: state -> unit
   val cancel_execution: state -> Future.task list
   val update_perspective: version_id -> version_id -> string -> command_id list -> state -> state
-  val edit: version_id -> version_id -> edit list -> state ->
+  val update: version_id -> version_id -> edit list -> state ->
     ((command_id * exec_id option) list * (string * command_id option) list) * state
   val execute: version_id -> state -> state
   val state: unit -> state
@@ -365,7 +365,7 @@
 
 
 
-(** editing **)
+(** update **)
 
 (* perspective *)
 
@@ -377,7 +377,7 @@
   in define_version new_id new_version state end;
 
 
-(* edit *)
+(* edits *)
 
 local
 
@@ -417,7 +417,7 @@
 
 in
 
-fun edit (old_id: version_id) (new_id: version_id) edits state =
+fun update (old_id: version_id) (new_id: version_id) edits state =
   let
     val old_version = the_version state old_id;
     val _ = Time.now ();  (* FIXME odd workaround for polyml-5.4.0/x86_64 *)
@@ -436,7 +436,7 @@
                 NONE => Future.value (([], [], []), set_touched false node)
               | SOME (entry as ((prev, id), _)) =>
                   (singleton o Future.forks)
-                    {name = "Document.edit", group = NONE,
+                    {name = "Document.update", group = NONE,
                       deps = map (Future.task_of o #2) deps, pri = 0, interrupts = false}
                     (fn () =>
                       let