# HG changeset patch
# User wenzelm
# Date 1285165040 -7200
# Node ID 1a34187f0b97955a776865852abbb7dd20db739c
# Parent  5638fe4f0843565de24399f5784d8a5707c86e34
basic setup for Session_Dockable controls;

diff -r 5638fe4f0843 -r 1a34187f0b97 src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Wed Sep 22 16:16:23 2010 +0200
+++ b/src/Pure/System/session.scala	Wed Sep 22 16:17:20 2010 +0200
@@ -115,6 +115,7 @@
   private val global_state = new Volatile(Document.State.init)
   def current_state(): Document.State = global_state.peek()
 
+  private case object Interrupt_Prover
   private case class Edit_Version(edits: List[Document.Node_Text_Edit])
   private case class Started(timeout: Int, args: List[String])
 
@@ -252,6 +253,9 @@
     var finished = false
     while (!finished) {
       receive {
+        case Interrupt_Prover =>
+          if (prover != null) prover.interrupt
+
         case Edit_Version(edits) =>
           val previous = global_state.peek().history.tip.current
           val result = Future.fork { Thy_Syntax.text_edits(Session.this, previous.join, edits) }
@@ -304,6 +308,8 @@
 
   def stop() { command_change_buffer ! Stop; session_actor ! Stop }
 
+  def interrupt() { session_actor ! Interrupt_Prover }
+
   def edit_version(edits: List[Document.Node_Text_Edit]) { session_actor !? Edit_Version(edits) }
 
   def snapshot(name: String, pending_edits: List[Text.Edit]): Document.Snapshot =
diff -r 5638fe4f0843 -r 1a34187f0b97 src/Tools/jEdit/src/jedit/session_dockable.scala
--- a/src/Tools/jEdit/src/jedit/session_dockable.scala	Wed Sep 22 16:16:23 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/session_dockable.scala	Wed Sep 22 16:17:20 2010 +0200
@@ -10,7 +10,10 @@
 import isabelle._
 
 import scala.actors.Actor._
-import scala.swing.{TextArea, ScrollPane, TabbedPane, Component}
+import scala.swing.{FlowPanel, Button, TextArea, ScrollPane, TabbedPane, Component}
+import scala.swing.event.ButtonClicked
+
+import java.awt.BorderLayout
 
 import org.gjt.sp.jedit.View
 
@@ -33,6 +36,17 @@
   set_content(tabs)
 
 
+  /* controls */
+
+  private val interrupt = new Button("Interrupt") {
+    reactions += { case ButtonClicked(_) => Isabelle.session.interrupt }
+  }
+  interrupt.tooltip = "Broadcast interrupt to all prover tasks"
+
+  private val controls = new FlowPanel(FlowPanel.Alignment.Right)(interrupt)
+  add(controls.peer, BorderLayout.NORTH)
+
+
   /* main actor */
 
   private val main_actor = actor {