# HG changeset patch
# User wenzelm
# Date 1375095636 -7200
# Node ID 8517172b9626278f645f5ec6579877c09b2cd28b
# Parent  a20631db9c8a884da3217c2f54204b63ac61b0ca
obsolete;

diff -r a20631db9c8a -r 8517172b9626 src/Pure/PIDE/execution.ML
--- a/src/Pure/PIDE/execution.ML	Mon Jul 29 12:50:16 2013 +0200
+++ b/src/Pure/PIDE/execution.ML	Mon Jul 29 13:00:36 2013 +0200
@@ -14,7 +14,6 @@
   val finished: Document_ID.exec -> unit
   val cancel: Document_ID.exec -> unit
   val terminate: Document_ID.exec -> unit
-  val snapshot: unit -> Future.group list
 end;
 
 structure Execution: EXECUTION =
@@ -65,8 +64,5 @@
 fun cancel exec_id = List.app Future.cancel_group (peek_list exec_id);
 fun terminate exec_id = List.app Future.terminate (peek_list exec_id);
 
-fun snapshot () =
-  Inttab.fold (cons o #2) (snd (Synchronized.value state)) [];
-
 end;
 
diff -r a20631db9c8a -r 8517172b9626 src/Pure/PIDE/protocol.ML
--- a/src/Pure/PIDE/protocol.ML	Mon Jul 29 12:50:16 2013 +0200
+++ b/src/Pure/PIDE/protocol.ML	Mon Jul 29 13:00:36 2013 +0200
@@ -20,16 +20,6 @@
     (fn [] => Execution.discontinue ());
 
 val _ =
-  Isabelle_Process.protocol_command "Document.cancel_execution"
-    (fn [] =>
-      let
-        val _ = Execution.discontinue ();
-        val groups = Execution.snapshot ();
-        val _ = List.app Future.cancel_group groups;
-        val _ = List.app Future.terminate groups;
-      in () end);
-
-val _ =
   Isabelle_Process.protocol_command "Document.update"
     (fn [old_id_string, new_id_string, edits_yxml] => Document.change_state (fn state =>
       let
diff -r a20631db9c8a -r 8517172b9626 src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Mon Jul 29 12:50:16 2013 +0200
+++ b/src/Pure/PIDE/protocol.scala	Mon Jul 29 13:00:36 2013 +0200
@@ -319,8 +319,6 @@
 
   def discontinue_execution() { protocol_command("Document.discontinue_execution") }
 
-  def cancel_execution() { protocol_command("Document.cancel_execution") }
-
   def update(old_id: Document_ID.Version, new_id: Document_ID.Version,
     edits: List[Document.Edit_Command])
   {
diff -r a20631db9c8a -r 8517172b9626 src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Mon Jul 29 12:50:16 2013 +0200
+++ b/src/Pure/System/session.scala	Mon Jul 29 13:00:36 2013 +0200
@@ -238,7 +238,6 @@
   /* actor messages */
 
   private case class Start(args: List[String])
-  private case object Cancel_Execution
   private case class Change(
     doc_edits: List[Document.Edit_Command],
     previous: Document.Version,
@@ -504,9 +503,6 @@
           global_options.event(Session.Global_Options(options))
           reply(())
 
-        case Cancel_Execution if prover.isDefined =>
-          prover.get.cancel_execution()
-
         case Session.Raw_Edits(edits) if prover.isDefined =>
           handle_raw_edits(edits)
           reply(())
@@ -553,8 +549,6 @@
     session_actor !? Stop
   }
 
-  def cancel_execution() { session_actor ! Cancel_Execution }
-
   def update(edits: List[Document.Edit_Text])
   { if (!edits.isEmpty) session_actor !? Session.Raw_Edits(edits) }