tuned signature;

--- 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

--- a/src/Pure/PIDE/isar_document.ML	Fri Aug 26 15:56:30 2011 +0200
+++ b/src/Pure/PIDE/isar_document.ML	Fri Aug 26 16:06:58 2011 +0200
@@ -28,7 +28,7 @@
       end));
 
 val _ =
-  Isabelle_Process.add_command "Isar_Document.edit_version"
+  Isabelle_Process.add_command "Isar_Document.update"
     (fn [old_id_string, new_id_string, edits_yxml] => Document.change_state (fn state =>
       let
         val old_id = Document.parse_id old_id_string;
@@ -48,7 +48,7 @@
             end;
 
         val running = Document.cancel_execution state;
-        val (assignment, state') = Document.edit old_id new_id edits state;
+        val (assignment, state') = Document.update old_id new_id edits state;
         val _ = Future.join_tasks running;
         val _ = Document.join_commands state';
         val _ =

--- a/src/Pure/PIDE/isar_document.scala	Fri Aug 26 15:56:30 2011 +0200
+++ b/src/Pure/PIDE/isar_document.scala	Fri Aug 26 16:06:58 2011 +0200
@@ -146,7 +146,7 @@
       YXML.string_of_body(ids))
   }
 
-  def edit_version(old_id: Document.Version_ID, new_id: Document.Version_ID,
+  def update(old_id: Document.Version_ID, new_id: Document.Version_ID,
     edits: List[Document.Edit_Command])
   {
     val edits_yxml =
@@ -163,7 +163,7 @@
             { case Document.Node.Perspective(a) => (a.commands.map(c => long_atom(c.id)), Nil) }))))
       YXML.string_of_body(encode(edits)) }
 
-    input("Isar_Document.edit_version", Document.ID(old_id), Document.ID(new_id), edits_yxml)
+    input("Isar_Document.update", Document.ID(old_id), Document.ID(new_id), edits_yxml)
   }
 
 

--- a/src/Pure/System/session.scala	Fri Aug 26 15:56:30 2011 +0200
+++ b/src/Pure/System/session.scala	Fri Aug 26 16:06:58 2011 +0200
@@ -282,7 +282,7 @@
 
       val assignment = global_state().the_assignment(previous).check_finished
       global_state.change(_.define_version(version, assignment))
-      prover.get.edit_version(previous.id, version.id, doc_edits)
+      prover.get.update(previous.id, version.id, doc_edits)
     }
     //}}}