--- 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) }