src/Tools/jEdit/src/theories_dockable.scala

 
 
 import isabelle._
 
 import scala.actors.Actor._
-import scala.swing.{FlowPanel, Button, TextArea, Label, ListView, Alignment, ScrollPane, Component}
+import scala.swing.{FlowPanel, Button, TextArea, Label, ListView, Alignment, ScrollPane, Component,
+  BoxPanel, Orientation, RadioButton, ButtonGroup}
 import scala.swing.event.{ButtonClicked, MouseClicked}
 
 import java.lang.System
-import java.awt.{BorderLayout, Graphics2D, Insets}
+import java.awt.{BorderLayout, Graphics2D, Insets, Color}
 import javax.swing.{JList, BorderFactory}
-import javax.swing.border.{BevelBorder, SoftBevelBorder}
+import javax.swing.border.{BevelBorder, SoftBevelBorder, LineBorder}
 
 import org.gjt.sp.jedit.{View, jEdit}
 
 
 class Theories_Dockable(view: View, position: String) extends Dockable(view, position)

   private def handle_phase(phase: Session.Phase)
   {
     Swing_Thread.later { session_phase.text = " " + phase_text(phase) + " " }
   }
 
-  private val cancel = new Button("Cancel") {
-    reactions += { case ButtonClicked(_) => PIDE.cancel_execution() }
+  private val execution_range = new BoxPanel(Orientation.Horizontal) {
+    private def button(range: PIDE.Execution_Range.Value): RadioButton =
+      new RadioButton(range.toString) {
+        reactions += { case ButtonClicked(_) => PIDE.update_execution_range(range) }
+      }
+    private val label = new Label("Range:") { tooltip = "range of continuous document processing" }
+    private val b1 = button(PIDE.Execution_Range.ALL)
+    private val b2 = button(PIDE.Execution_Range.NONE)
+    private val b3 = button(PIDE.Execution_Range.VISIBLE)
+    private val group = new ButtonGroup(b1, b2, b3)
+    contents ++= List(label, b1, b2, b3)
+    border = new LineBorder(Color.GRAY)
+
+    def load()
+    {
+      PIDE.execution_range() match {
+        case PIDE.Execution_Range.ALL => group.select(b1)
+        case PIDE.Execution_Range.NONE => group.select(b2)
+        case PIDE.Execution_Range.VISIBLE => group.select(b3)
+      }
+    }
   }
-  cancel.tooltip = "Cancel current checking process"
-
-  private val check = new Button("Check") {
-    reactions += { case ButtonClicked(_) => PIDE.check_buffer(view.getBuffer) }
-  }
-  check.tooltip = "Commence full checking of current buffer"
 
   private val logic = Isabelle_Logic.logic_selector(true)
 
   private val controls =
-    new FlowPanel(FlowPanel.Alignment.Right)(check, cancel, session_phase, logic)
+    new FlowPanel(FlowPanel.Alignment.Right)(execution_range, session_phase, logic)
   add(controls.peer, BorderLayout.NORTH)
 
 
   /* component state -- owned by Swing thread */
 

   private val main_actor = actor {
     loop {
       react {
         case phase: Session.Phase => handle_phase(phase)
 
-        case _: Session.Global_Options => Swing_Thread.later { logic.load () }
+        case _: Session.Global_Options =>
+          Swing_Thread.later {
+            execution_range.load()
+            logic.load ()
+          }
 
         case changed: Session.Commands_Changed => handle_update(Some(changed.nodes))
 
         case bad => System.err.println("Theories_Dockable: ignoring bad message " + bad)
       }