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