explicit cancel_execution before queueing new edits -- potential performance improvement for machines with few cores;

--- a/src/Pure/PIDE/isar_document.ML	Wed Aug 31 20:32:24 2011 +0200
+++ b/src/Pure/PIDE/isar_document.ML	Wed Aug 31 20:47:33 2011 +0200
@@ -12,6 +12,10 @@
     (fn [id, text] => Document.change_state (Document.define_command (Document.parse_id id) text));
 
 val _ =
+  Isabelle_Process.add_command "Isar_Document.cancel_execution"
+    (fn [] => ignore (Document.cancel_execution (Document.state ())));
+
+val _ =
   Isabelle_Process.add_command "Isar_Document.update_perspective"
     (fn [old_id_string, new_id_string, name, ids_yxml] => Document.change_state (fn state =>
       let

--- a/src/Pure/PIDE/isar_document.scala	Wed Aug 31 20:32:24 2011 +0200
+++ b/src/Pure/PIDE/isar_document.scala	Wed Aug 31 20:47:33 2011 +0200
@@ -135,6 +135,11 @@
 
   /* document versions */
 
+  def cancel_execution()
+  {
+    input("Isar_Document.cancel_execution")
+  }
+
   def update_perspective(old_id: Document.Version_ID, new_id: Document.Version_ID,
     name: String, perspective: Command.Perspective)
   {

--- a/src/Pure/System/session.scala	Wed Aug 31 20:32:24 2011 +0200
+++ b/src/Pure/System/session.scala	Wed Aug 31 20:47:33 2011 +0200
@@ -213,6 +213,8 @@
       val syntax = current_syntax()
       val previous = global_state().history.tip.version
 
+      prover.get.cancel_execution()
+
       val text_edits = header_edit(name, master_dir, header) :: edits.map(edit => (name, edit))
       val result = Future.fork { Thy_Syntax.text_edits(syntax, previous.join, text_edits) }
       val change =