src/Pure/PIDE/document.ML

   val init_state: state
   val define_command: command_id -> string -> state -> state
   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
   val change_state: (state -> state) -> unit
 end;

 end;
 
 
 
 
-(** editing **)
+(** update **)
 
 (* perspective *)
 
 fun update_perspective (old_id: version_id) (new_id: version_id) name perspective state =
   let

     val _ = Time.now ();  (* FIXME odd workaround for polyml-5.4.0/x86_64 -- needed? *)
     val new_version = edit_nodes (name, Perspective perspective) old_version;
   in define_version new_id new_version state end;
 
 
-(* edit *)
+(* edits *)
 
 local
 
 fun init_theory deps name node =
   let

       |> pair command_id';
   in ((exec_id', exec') :: execs, exec') end;
 
 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 *)
     val new_version = fold edit_nodes edits old_version;
 

             in
               (case first_entry NONE (after_perspective node orf needs_update node0) node of
                 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
                         val update_start =
                           Option.map (#2 o #1) (first_entry (SOME id) (needs_update node0) node);