1.1 --- a/src/Pure/System/isabelle_process.scala	Wed Sep 07 09:10:41 2011 +0200
     1.2 +++ b/src/Pure/System/isabelle_process.scala	Wed Sep 07 11:00:39 2011 +0200
     1.3 @@ -205,12 +205,6 @@
     1.4  
     1.5    def join() { process_manager.join() }
     1.6  
     1.7 -  def interrupt()
     1.8 -  {
     1.9 -    try { process.interrupt }
    1.10 -    catch { case e: IOException => system_result("Failed to interrupt Isabelle: " + e.getMessage) }
    1.11 -  }
    1.12 -
    1.13    def terminate()
    1.14    {
    1.15      close()

     2.1 --- a/src/Pure/System/session.scala	Wed Sep 07 09:10:41 2011 +0200
     2.2 +++ b/src/Pure/System/session.scala	Wed Sep 07 11:00:39 2011 +0200
     2.3 @@ -137,7 +137,7 @@
     2.4    /* actor messages */
     2.5  
     2.6    private case class Start(timeout: Time, args: List[String])
     2.7 -  private case object Interrupt
     2.8 +  private case object Cancel_Execution
     2.9    private case class Init_Node(name: Document.Node.Name,
    2.10      header: Document.Node_Header, perspective: Text.Perspective, text: String)
    2.11    private case class Edit_Node(name: Document.Node.Name,
    2.12 @@ -423,8 +423,8 @@
    2.13            receiver.cancel()
    2.14            reply(())
    2.15  
    2.16 -        case Interrupt if prover.isDefined =>
    2.17 -          prover.get.interrupt
    2.18 +        case Cancel_Execution if prover.isDefined =>
    2.19 +          prover.get.cancel_execution()
    2.20  
    2.21          case Init_Node(name, header, perspective, text) if prover.isDefined =>
    2.22            // FIXME compare with existing node
    2.23 @@ -471,7 +471,7 @@
    2.24  
    2.25    def stop() { commands_changed_buffer !? Stop; session_actor !? Stop }
    2.26  
    2.27 -  def interrupt() { session_actor ! Interrupt }
    2.28 +  def cancel_execution() { session_actor ! Cancel_Execution }
    2.29  
    2.30    def init_node(name: Document.Node.Name,
    2.31      header: Document.Node_Header, perspective: Text.Perspective, text: String)

     3.1 --- a/src/Tools/jEdit/src/session_dockable.scala	Wed Sep 07 09:10:41 2011 +0200
     3.2 +++ b/src/Tools/jEdit/src/session_dockable.scala	Wed Sep 07 11:00:39 2011 +0200
     3.3 @@ -61,13 +61,19 @@
     3.4    session_phase.border = new SoftBevelBorder(BevelBorder.LOWERED)
     3.5    session_phase.tooltip = "Prover status"
     3.6  
     3.7 +  private val cancel = new Button("Cancel") {
     3.8 +    reactions += { case ButtonClicked(_) => Isabelle.session.cancel_execution }
     3.9 +  }
    3.10 +  cancel.tooltip = "Cancel current proof checking process"
    3.11 +
    3.12    private val logic = Isabelle.logic_selector(Isabelle.Property("logic"))
    3.13    logic.listenTo(logic.selection)
    3.14    logic.reactions += {
    3.15      case SelectionChanged(_) => Isabelle.Property("logic") = logic.selection.item.name
    3.16    }
    3.17  
    3.18 -  private val controls = new FlowPanel(FlowPanel.Alignment.Right)(session_phase, logic)
    3.19 +  private val controls =
    3.20 +    new FlowPanel(FlowPanel.Alignment.Right)(session_phase, cancel, logic)
    3.21    add(controls.peer, BorderLayout.NORTH)
    3.22  
    3.23