src/Tools/jEdit/src/theories_dockable.scala
changeset 52807 b859a180936b
parent 52802 0b98561d0790
child 52809 e750169a5884
     1.1 --- a/src/Tools/jEdit/src/theories_dockable.scala	Tue Jul 30 23:17:26 2013 +0200
     1.2 +++ b/src/Tools/jEdit/src/theories_dockable.scala	Wed Jul 31 10:54:37 2013 +0200
     1.3 @@ -10,8 +10,8 @@
     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 -  BoxPanel, Orientation, RadioButton, ButtonGroup}
     1.9 +import scala.swing.{FlowPanel, Button, TextArea, Label, ListView, Alignment,
    1.10 +  ScrollPane, Component, CheckBox}
    1.11  import scala.swing.event.{ButtonClicked, MouseClicked}
    1.12  
    1.13  import java.lang.System
    1.14 @@ -55,36 +55,17 @@
    1.15      Swing_Thread.later { session_phase.text = " " + phase_text(phase) + " " }
    1.16    }
    1.17  
    1.18 -  private val execution_range = new BoxPanel(Orientation.Horizontal) {
    1.19 -    private def button(range: PIDE.Execution_Range.Value, tip: String): RadioButton =
    1.20 -      new RadioButton(range.toString) {
    1.21 -        tooltip = tip
    1.22 -        reactions += { case ButtonClicked(_) => PIDE.update_execution_range(range) }
    1.23 -      }
    1.24 -    private val label =
    1.25 -      new Label("Range:") { tooltip = "Execution range of continuous document processing" }
    1.26 -    private val b1 = button(PIDE.Execution_Range.ALL, "Check all theories (potentially slow)")
    1.27 -    private val b2 = button(PIDE.Execution_Range.NONE, "Check nothing")
    1.28 -    private val b3 = button(PIDE.Execution_Range.VISIBLE, "Check visible parts of theories")
    1.29 -    private val group = new ButtonGroup(b1, b2, b3)
    1.30 -    contents ++= List(label, b1, b2, b3)
    1.31 -    border = new SoftBevelBorder(BevelBorder.LOWERED)
    1.32 -
    1.33 -    def load()
    1.34 -    {
    1.35 -      PIDE.execution_range() match {
    1.36 -        case PIDE.Execution_Range.ALL => group.select(b1)
    1.37 -        case PIDE.Execution_Range.NONE => group.select(b2)
    1.38 -        case PIDE.Execution_Range.VISIBLE => group.select(b3)
    1.39 -      }
    1.40 -    }
    1.41 +  private val continuous_checking = new CheckBox("Continuous checking") {
    1.42 +    tooltip = "Continuous checking of proof document (visible and required parts)"
    1.43 +    reactions += { case ButtonClicked(_) => PIDE.continuous_checking = selected }
    1.44 +    def load() { selected = PIDE.continuous_checking }
    1.45      load()
    1.46    }
    1.47  
    1.48    private val logic = Isabelle_Logic.logic_selector(true)
    1.49  
    1.50    private val controls =
    1.51 -    new FlowPanel(FlowPanel.Alignment.Right)(execution_range, session_phase, logic)
    1.52 +    new FlowPanel(FlowPanel.Alignment.Right)(continuous_checking, session_phase, logic)
    1.53    add(controls.peer, BorderLayout.NORTH)
    1.54  
    1.55  
    1.56 @@ -175,7 +156,7 @@
    1.57  
    1.58          case _: Session.Global_Options =>
    1.59            Swing_Thread.later {
    1.60 -            execution_range.load()
    1.61 +            continuous_checking.load()
    1.62              logic.load ()
    1.63            }
    1.64