# HG changeset patch
# User wenzelm
# Date 1315386039 -7200
# Node ID 27930cf6f0f70e7fef0950ad013b7d85c7957a27
# Parent  72785558a6fff38ecbe51bb65971672bff99f332
added "cancel" button based on cancel_execution, not interrupt (cf. 156be0e43336);

diff -r 72785558a6ff -r 27930cf6f0f7 src/Pure/System/isabelle_process.scala
--- a/src/Pure/System/isabelle_process.scala	Wed Sep 07 09:10:41 2011 +0200
+++ b/src/Pure/System/isabelle_process.scala	Wed Sep 07 11:00:39 2011 +0200
@@ -205,12 +205,6 @@
 
   def join() { process_manager.join() }
 
-  def interrupt()
-  {
-    try { process.interrupt }
-    catch { case e: IOException => system_result("Failed to interrupt Isabelle: " + e.getMessage) }
-  }
-
   def terminate()
   {
     close()
diff -r 72785558a6ff -r 27930cf6f0f7 src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Wed Sep 07 09:10:41 2011 +0200
+++ b/src/Pure/System/session.scala	Wed Sep 07 11:00:39 2011 +0200
@@ -137,7 +137,7 @@
   /* actor messages */
 
   private case class Start(timeout: Time, args: List[String])
-  private case object Interrupt
+  private case object Cancel_Execution
   private case class Init_Node(name: Document.Node.Name,
     header: Document.Node_Header, perspective: Text.Perspective, text: String)
   private case class Edit_Node(name: Document.Node.Name,
@@ -423,8 +423,8 @@
           receiver.cancel()
           reply(())
 
-        case Interrupt if prover.isDefined =>
-          prover.get.interrupt
+        case Cancel_Execution if prover.isDefined =>
+          prover.get.cancel_execution()
 
         case Init_Node(name, header, perspective, text) if prover.isDefined =>
           // FIXME compare with existing node
@@ -471,7 +471,7 @@
 
   def stop() { commands_changed_buffer !? Stop; session_actor !? Stop }
 
-  def interrupt() { session_actor ! Interrupt }
+  def cancel_execution() { session_actor ! Cancel_Execution }
 
   def init_node(name: Document.Node.Name,
     header: Document.Node_Header, perspective: Text.Perspective, text: String)
diff -r 72785558a6ff -r 27930cf6f0f7 src/Tools/jEdit/src/session_dockable.scala
--- a/src/Tools/jEdit/src/session_dockable.scala	Wed Sep 07 09:10:41 2011 +0200
+++ b/src/Tools/jEdit/src/session_dockable.scala	Wed Sep 07 11:00:39 2011 +0200
@@ -61,13 +61,19 @@
   session_phase.border = new SoftBevelBorder(BevelBorder.LOWERED)
   session_phase.tooltip = "Prover status"
 
+  private val cancel = new Button("Cancel") {
+    reactions += { case ButtonClicked(_) => Isabelle.session.cancel_execution }
+  }
+  cancel.tooltip = "Cancel current proof checking process"
+
   private val logic = Isabelle.logic_selector(Isabelle.Property("logic"))
   logic.listenTo(logic.selection)
   logic.reactions += {
     case SelectionChanged(_) => Isabelle.Property("logic") = logic.selection.item.name
   }
 
-  private val controls = new FlowPanel(FlowPanel.Alignment.Right)(session_phase, logic)
+  private val controls =
+    new FlowPanel(FlowPanel.Alignment.Right)(session_phase, cancel, logic)
   add(controls.peer, BorderLayout.NORTH)