src/Pure/System/session.scala
changeset 39593 1a34187f0b97
parent 39589 5b81b8df1dde
child 39625 fb0c851e4f9d
     1.1 --- a/src/Pure/System/session.scala	Wed Sep 22 16:16:23 2010 +0200
     1.2 +++ b/src/Pure/System/session.scala	Wed Sep 22 16:17:20 2010 +0200
     1.3 @@ -115,6 +115,7 @@
     1.4    private val global_state = new Volatile(Document.State.init)
     1.5    def current_state(): Document.State = global_state.peek()
     1.6  
     1.7 +  private case object Interrupt_Prover
     1.8    private case class Edit_Version(edits: List[Document.Node_Text_Edit])
     1.9    private case class Started(timeout: Int, args: List[String])
    1.10  
    1.11 @@ -252,6 +253,9 @@
    1.12      var finished = false
    1.13      while (!finished) {
    1.14        receive {
    1.15 +        case Interrupt_Prover =>
    1.16 +          if (prover != null) prover.interrupt
    1.17 +
    1.18          case Edit_Version(edits) =>
    1.19            val previous = global_state.peek().history.tip.current
    1.20            val result = Future.fork { Thy_Syntax.text_edits(Session.this, previous.join, edits) }
    1.21 @@ -304,6 +308,8 @@
    1.22  
    1.23    def stop() { command_change_buffer ! Stop; session_actor ! Stop }
    1.24  
    1.25 +  def interrupt() { session_actor ! Interrupt_Prover }
    1.26 +
    1.27    def edit_version(edits: List[Document.Node_Text_Edit]) { session_actor !? Edit_Version(edits) }
    1.28  
    1.29    def snapshot(name: String, pending_edits: List[Text.Edit]): Document.Snapshot =