src/Tools/jEdit/src/theories_dockable.scala
changeset 52759 a20631db9c8a
parent 51535 f2f480bc4223
child 52763 3b5f4f2ff108
     1.1 --- a/src/Tools/jEdit/src/theories_dockable.scala	Sun Jul 28 20:51:15 2013 +0200
     1.2 +++ b/src/Tools/jEdit/src/theories_dockable.scala	Mon Jul 29 12:50:16 2013 +0200
     1.3 @@ -10,13 +10,14 @@
     1.4  import isabelle._
     1.5  
     1.6  import scala.actors.Actor._
     1.7 -import scala.swing.{FlowPanel, Button, TextArea, Label, ListView, Alignment, ScrollPane, Component}
     1.8 +import scala.swing.{FlowPanel, Button, TextArea, Label, ListView, Alignment, ScrollPane, Component,
     1.9 +  BoxPanel, Orientation, RadioButton, ButtonGroup}
    1.10  import scala.swing.event.{ButtonClicked, MouseClicked}
    1.11  
    1.12  import java.lang.System
    1.13 -import java.awt.{BorderLayout, Graphics2D, Insets}
    1.14 +import java.awt.{BorderLayout, Graphics2D, Insets, Color}
    1.15  import javax.swing.{JList, BorderFactory}
    1.16 -import javax.swing.border.{BevelBorder, SoftBevelBorder}
    1.17 +import javax.swing.border.{BevelBorder, SoftBevelBorder, LineBorder}
    1.18  
    1.19  import org.gjt.sp.jedit.{View, jEdit}
    1.20  
    1.21 @@ -54,20 +55,33 @@
    1.22      Swing_Thread.later { session_phase.text = " " + phase_text(phase) + " " }
    1.23    }
    1.24  
    1.25 -  private val cancel = new Button("Cancel") {
    1.26 -    reactions += { case ButtonClicked(_) => PIDE.cancel_execution() }
    1.27 -  }
    1.28 -  cancel.tooltip = "Cancel current checking process"
    1.29 +  private val execution_range = new BoxPanel(Orientation.Horizontal) {
    1.30 +    private def button(range: PIDE.Execution_Range.Value): RadioButton =
    1.31 +      new RadioButton(range.toString) {
    1.32 +        reactions += { case ButtonClicked(_) => PIDE.update_execution_range(range) }
    1.33 +      }
    1.34 +    private val label = new Label("Range:") { tooltip = "range of continuous document processing" }
    1.35 +    private val b1 = button(PIDE.Execution_Range.ALL)
    1.36 +    private val b2 = button(PIDE.Execution_Range.NONE)
    1.37 +    private val b3 = button(PIDE.Execution_Range.VISIBLE)
    1.38 +    private val group = new ButtonGroup(b1, b2, b3)
    1.39 +    contents ++= List(label, b1, b2, b3)
    1.40 +    border = new LineBorder(Color.GRAY)
    1.41  
    1.42 -  private val check = new Button("Check") {
    1.43 -    reactions += { case ButtonClicked(_) => PIDE.check_buffer(view.getBuffer) }
    1.44 +    def load()
    1.45 +    {
    1.46 +      PIDE.execution_range() match {
    1.47 +        case PIDE.Execution_Range.ALL => group.select(b1)
    1.48 +        case PIDE.Execution_Range.NONE => group.select(b2)
    1.49 +        case PIDE.Execution_Range.VISIBLE => group.select(b3)
    1.50 +      }
    1.51 +    }
    1.52    }
    1.53 -  check.tooltip = "Commence full checking of current buffer"
    1.54  
    1.55    private val logic = Isabelle_Logic.logic_selector(true)
    1.56  
    1.57    private val controls =
    1.58 -    new FlowPanel(FlowPanel.Alignment.Right)(check, cancel, session_phase, logic)
    1.59 +    new FlowPanel(FlowPanel.Alignment.Right)(execution_range, session_phase, logic)
    1.60    add(controls.peer, BorderLayout.NORTH)
    1.61  
    1.62  
    1.63 @@ -156,7 +170,11 @@
    1.64        react {
    1.65          case phase: Session.Phase => handle_phase(phase)
    1.66  
    1.67 -        case _: Session.Global_Options => Swing_Thread.later { logic.load () }
    1.68 +        case _: Session.Global_Options =>
    1.69 +          Swing_Thread.later {
    1.70 +            execution_range.load()
    1.71 +            logic.load ()
    1.72 +          }
    1.73  
    1.74          case changed: Session.Commands_Changed => handle_update(Some(changed.nodes))
    1.75