src/Pure/System/session.scala

--- a/src/Pure/System/session.scala	Wed Sep 22 16:16:23 2010 +0200
+++ b/src/Pure/System/session.scala	Wed Sep 22 16:17:20 2010 +0200
@@ -115,6 +115,7 @@
   private val global_state = new Volatile(Document.State.init)
   def current_state(): Document.State = global_state.peek()
 
+  private case object Interrupt_Prover
   private case class Edit_Version(edits: List[Document.Node_Text_Edit])
   private case class Started(timeout: Int, args: List[String])
 
@@ -252,6 +253,9 @@
     var finished = false
     while (!finished) {
       receive {
+        case Interrupt_Prover =>
+          if (prover != null) prover.interrupt
+
         case Edit_Version(edits) =>
           val previous = global_state.peek().history.tip.current
           val result = Future.fork { Thy_Syntax.text_edits(Session.this, previous.join, edits) }
@@ -304,6 +308,8 @@
 
   def stop() { command_change_buffer ! Stop; session_actor ! Stop }
 
+  def interrupt() { session_actor ! Interrupt_Prover }
+
   def edit_version(edits: List[Document.Node_Text_Edit]) { session_actor !? Edit_Version(edits) }
 
   def snapshot(name: String, pending_edits: List[Text.Edit]): Document.Snapshot =