obsolete;
authorwenzelm
Mon Jul 29 13:00:36 2013 +0200 (2013-07-29 ago)
changeset 527608517172b9626
parent 52759 a20631db9c8a
child 52761 909167fdd367
obsolete;
src/Pure/PIDE/execution.ML
src/Pure/PIDE/protocol.ML
src/Pure/PIDE/protocol.scala
src/Pure/System/session.scala
     1.1 --- a/src/Pure/PIDE/execution.ML	Mon Jul 29 12:50:16 2013 +0200
     1.2 +++ b/src/Pure/PIDE/execution.ML	Mon Jul 29 13:00:36 2013 +0200
     1.3 @@ -14,7 +14,6 @@
     1.4    val finished: Document_ID.exec -> unit
     1.5    val cancel: Document_ID.exec -> unit
     1.6    val terminate: Document_ID.exec -> unit
     1.7 -  val snapshot: unit -> Future.group list
     1.8  end;
     1.9  
    1.10  structure Execution: EXECUTION =
    1.11 @@ -65,8 +64,5 @@
    1.12  fun cancel exec_id = List.app Future.cancel_group (peek_list exec_id);
    1.13  fun terminate exec_id = List.app Future.terminate (peek_list exec_id);
    1.14  
    1.15 -fun snapshot () =
    1.16 -  Inttab.fold (cons o #2) (snd (Synchronized.value state)) [];
    1.17 -
    1.18  end;
    1.19  
     2.1 --- a/src/Pure/PIDE/protocol.ML	Mon Jul 29 12:50:16 2013 +0200
     2.2 +++ b/src/Pure/PIDE/protocol.ML	Mon Jul 29 13:00:36 2013 +0200
     2.3 @@ -20,16 +20,6 @@
     2.4      (fn [] => Execution.discontinue ());
     2.5  
     2.6  val _ =
     2.7 -  Isabelle_Process.protocol_command "Document.cancel_execution"
     2.8 -    (fn [] =>
     2.9 -      let
    2.10 -        val _ = Execution.discontinue ();
    2.11 -        val groups = Execution.snapshot ();
    2.12 -        val _ = List.app Future.cancel_group groups;
    2.13 -        val _ = List.app Future.terminate groups;
    2.14 -      in () end);
    2.15 -
    2.16 -val _ =
    2.17    Isabelle_Process.protocol_command "Document.update"
    2.18      (fn [old_id_string, new_id_string, edits_yxml] => Document.change_state (fn state =>
    2.19        let
     3.1 --- a/src/Pure/PIDE/protocol.scala	Mon Jul 29 12:50:16 2013 +0200
     3.2 +++ b/src/Pure/PIDE/protocol.scala	Mon Jul 29 13:00:36 2013 +0200
     3.3 @@ -319,8 +319,6 @@
     3.4  
     3.5    def discontinue_execution() { protocol_command("Document.discontinue_execution") }
     3.6  
     3.7 -  def cancel_execution() { protocol_command("Document.cancel_execution") }
     3.8 -
     3.9    def update(old_id: Document_ID.Version, new_id: Document_ID.Version,
    3.10      edits: List[Document.Edit_Command])
    3.11    {
     4.1 --- a/src/Pure/System/session.scala	Mon Jul 29 12:50:16 2013 +0200
     4.2 +++ b/src/Pure/System/session.scala	Mon Jul 29 13:00:36 2013 +0200
     4.3 @@ -238,7 +238,6 @@
     4.4    /* actor messages */
     4.5  
     4.6    private case class Start(args: List[String])
     4.7 -  private case object Cancel_Execution
     4.8    private case class Change(
     4.9      doc_edits: List[Document.Edit_Command],
    4.10      previous: Document.Version,
    4.11 @@ -504,9 +503,6 @@
    4.12            global_options.event(Session.Global_Options(options))
    4.13            reply(())
    4.14  
    4.15 -        case Cancel_Execution if prover.isDefined =>
    4.16 -          prover.get.cancel_execution()
    4.17 -
    4.18          case Session.Raw_Edits(edits) if prover.isDefined =>
    4.19            handle_raw_edits(edits)
    4.20            reply(())
    4.21 @@ -553,8 +549,6 @@
    4.22      session_actor !? Stop
    4.23    }
    4.24  
    4.25 -  def cancel_execution() { session_actor ! Cancel_Execution }
    4.26 -
    4.27    def update(edits: List[Document.Edit_Text])
    4.28    { if (!edits.isEmpty) session_actor !? Session.Raw_Edits(edits) }
    4.29