# HG changeset patch
# User wenzelm
# Date 1333628091 -7200
# Node ID b8aeab386414712eb3652317a2d33239dfbe5f2e
# Parent  7828c7b3c1432ba14d0a79df9fbb88f5ec8c5eb3
less aggressive discontinue_execution before document update, to avoid unstable execs that need to be re-assigned;

diff -r 7828c7b3c143 -r b8aeab386414 src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Thu Apr 05 13:01:54 2012 +0200
+++ b/src/Pure/PIDE/document.ML	Thu Apr 05 14:14:51 2012 +0200
@@ -25,6 +25,7 @@
   type state
   val init_state: state
   val define_command: command_id -> string -> string -> state -> state
+  val discontinue_execution: state -> unit
   val cancel_execution: state -> Future.task list
   val update_perspective: version_id -> version_id -> string -> command_id list -> state -> state
   val update: version_id -> version_id -> edit list -> state ->
@@ -242,7 +243,7 @@
 abstype state = State of
  {versions: version Inttab.table,  (*version_id -> document content*)
   commands: (string * Token.T list lazy) Inttab.table,  (*command_id -> named span*)
-  execution: version_id * Future.group}  (*current execution process*)
+  execution: version_id * Future.group * bool Unsynchronized.ref}  (*current execution process*)
 with
 
 fun make_state (versions, commands, execution) =
@@ -252,7 +253,8 @@
   make_state (f (versions, commands, execution));
 
 val init_state =
-  make_state (Inttab.make [(no_id, empty_version)], Inttab.empty, (no_id, Future.new_group NONE));
+  make_state (Inttab.make [(no_id, empty_version)], Inttab.empty,
+    (no_id, Future.new_group NONE, Unsynchronized.ref false));
 
 
 (* document versions *)
@@ -291,7 +293,9 @@
 
 (* document execution *)
 
-fun cancel_execution (State {execution, ...}) = Future.cancel_group (#2 execution);
+fun discontinue_execution  (State {execution = (_, _, running), ...}) = running := false;
+
+fun cancel_execution (State {execution = (_, group, _), ...}) = Future.cancel_group group;
 
 end;
 
@@ -483,8 +487,11 @@
     let
       val version = the_version state version_id;
 
-      fun force_exec _ _ NONE = ()
-        | force_exec node command_id (SOME (_, exec)) =
+      val group = Future.new_group NONE;
+      val running = Unsynchronized.ref true;
+
+      fun run _ _ NONE = ()
+        | run node command_id (SOME (_, exec)) =
             let
               val (_, print) = Command.memo_eval exec;
               val _ =
@@ -493,17 +500,17 @@
                 else ();
             in () end;
 
-      val group = Future.new_group NONE;
       val _ =
         nodes_of version |> Graph.schedule
           (fn deps => fn (name, node) =>
             (singleton o Future.forks)
               {name = "theory:" ^ name, group = SOME (Future.new_group (SOME group)),
                 deps = map (Future.task_of o #2) deps, pri = 1, interrupts = false}
-              (iterate_entries (fn ((_, id), exec) => fn () =>
-                SOME (force_exec node id exec)) node));
+              (fn () =>
+                iterate_entries (fn ((_, id), exec) => fn () =>
+                  if ! running then SOME (run node id exec) else NONE) node ()));
 
-    in (versions, commands, (version_id, group)) end);
+    in (versions, commands, (version_id, group, running)) end);
 
 
 (* remove versions *)
diff -r 7828c7b3c143 -r b8aeab386414 src/Pure/PIDE/protocol.ML
--- a/src/Pure/PIDE/protocol.ML	Thu Apr 05 13:01:54 2012 +0200
+++ b/src/Pure/PIDE/protocol.ML	Thu Apr 05 14:14:51 2012 +0200
@@ -13,6 +13,10 @@
       Document.change_state (Document.define_command (Document.parse_id id) name text));
 
 val _ =
+  Isabelle_Process.protocol_command "Document.discontinue_execution"
+    (fn [] => Document.discontinue_execution (Document.state ()));
+
+val _ =
   Isabelle_Process.protocol_command "Document.cancel_execution"
     (fn [] => ignore (Document.cancel_execution (Document.state ())));
 
diff -r 7828c7b3c143 -r b8aeab386414 src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Thu Apr 05 13:01:54 2012 +0200
+++ b/src/Pure/PIDE/protocol.scala	Thu Apr 05 14:14:51 2012 +0200
@@ -191,10 +191,9 @@
 
   /* document versions */
 
-  def cancel_execution()
-  {
-    input("Document.cancel_execution")
-  }
+  def discontinue_execution() { input("Document.discontinue_execution") }
+
+  def cancel_execution() { input("Document.cancel_execution") }
 
   def update_perspective(old_id: Document.Version_ID, new_id: Document.Version_ID,
     name: Document.Node.Name, perspective: Command.Perspective)
diff -r 7828c7b3c143 -r b8aeab386414 src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Thu Apr 05 13:01:54 2012 +0200
+++ b/src/Pure/System/session.scala	Thu Apr 05 14:14:51 2012 +0200
@@ -296,7 +296,7 @@
     {
       val previous = global_state().history.tip.version
 
-      prover.get.cancel_execution()
+      prover.get.discontinue_execution()
 
       val text_edits = header_edit(name, header) :: edits.map(edit => (name, edit))
       val version = Future.promise[Document.Version]