cancel document execution before editing, to improve reactivity on systems with few cores;

--- a/src/Pure/PIDE/document.ML	Tue Jan 25 22:59:03 2011 +0100
+++ b/src/Pure/PIDE/document.ML	Thu Jan 27 12:24:00 2011 +0100
@@ -18,6 +18,7 @@
   type edit = string * ((command_id option * command_id option) list) option
   type state
   val init_state: state
+  val cancel: state -> unit
   val define_command: command_id -> string -> state -> state
   val edit: version_id -> version_id -> edit list -> state -> (command_id * exec_id) list * state
   val execute: version_id -> state -> state
@@ -181,6 +182,15 @@
     NONE => err_undef "command execution" id
   | SOME exec => exec);
 
+
+(* document execution *)
+
+fun cancel (State {execution, ...}) =
+  List.app Future.cancel execution;
+
+fun await_cancellation (State {execution, ...}) =
+  ignore (Future.join_results execution);
+
 end;
 
 
@@ -324,20 +334,19 @@
       fun force_exec NONE = ()
         | force_exec (SOME exec_id) = ignore (Lazy.force (the_exec state exec_id));
 
-      val _ = List.app Future.cancel execution;
-      fun await_cancellation () = Future.join_results execution;
+      val _ = cancel state;
 
       val execution' = (* FIXME proper node deps *)
         [Future.fork_pri 1 (fn () =>
           let
-            val _ = await_cancellation ();
+            val _ = await_cancellation state;
             val _ =
               node_names_of version |> List.app (fn name =>
                 fold_entries NONE (fn (_, exec) => fn () => force_exec exec)
                     (get_node version name) ());
           in () end)];
 
-      val _ = await_cancellation ();
+      val _ = await_cancellation state;  (* FIXME async!? *)
 
     in (versions, commands, execs, execution') end);
 

--- a/src/Pure/PIDE/isar_document.ML	Tue Jan 25 22:59:03 2011 +0100
+++ b/src/Pure/PIDE/isar_document.ML	Thu Jan 27 12:24:00 2011 +0100
@@ -30,6 +30,7 @@
                     (XML_Data.dest_option XML_Data.dest_int)
                     (XML_Data.dest_option XML_Data.dest_int))))) (YXML.parse_body edits_yxml);
 
+      val _ = Document.cancel state;
       val (updates, state') = Document.edit old_id new_id edits state;
       val _ =
         implode (map (fn (id, exec_id) => Markup.markup (Markup.edit id exec_id) "") updates)