# 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)