# HG changeset patch
# User wenzelm
# Date 1313864652 -7200
# Node ID 156be0e433361d29a55cae58880f59de46a37716
# Parent  605381e7c7c5e7afba651c5e3ea68c4830f4b2c9
discontinued "Interrupt", which could disturb administrative tasks of the document model;

diff -r 605381e7c7c5 -r 156be0e43336 src/Tools/jEdit/src/session_dockable.scala
--- a/src/Tools/jEdit/src/session_dockable.scala	Sat Aug 20 20:00:55 2011 +0200
+++ b/src/Tools/jEdit/src/session_dockable.scala	Sat Aug 20 20:24:12 2011 +0200
@@ -54,19 +54,13 @@
   session_phase.border = new SoftBevelBorder(BevelBorder.LOWERED)
   session_phase.tooltip = "Prover status"
 
-  private val interrupt = new Button("Interrupt") {
-    reactions += { case ButtonClicked(_) => Isabelle.session.interrupt }
-  }
-  interrupt.tooltip = "Broadcast interrupt to all prover tasks"
-
   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, interrupt, logic)
+  private val controls = new FlowPanel(FlowPanel.Alignment.Right)(session_phase, logic)
   add(controls.peer, BorderLayout.NORTH)