# HG changeset patch
# User wenzelm
# Date 1314816453 -7200
# Node ID 990ac978854c69e710a27ce5ed39e2ba97e1b9b6
# Parent  857c52a1c3f7bb35e83935f766cdb9ca063ca528
explicit cancel_execution before queueing new edits -- potential performance improvement for machines with few cores;

diff -r 857c52a1c3f7 -r 990ac978854c src/Pure/PIDE/isar_document.ML
--- 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
diff -r 857c52a1c3f7 -r 990ac978854c src/Pure/PIDE/isar_document.scala
--- 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)
   {
diff -r 857c52a1c3f7 -r 990ac978854c src/Pure/System/session.scala
--- 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 =