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 =