added "cancel" button based on cancel_execution, not interrupt (cf. 156be0e43336);
--- 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()
--- 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)
--- 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)