8 |
8 |
9 |
9 |
10 import isabelle._ |
10 import isabelle._ |
11 |
11 |
12 import scala.actors.Actor._ |
12 import scala.actors.Actor._ |
13 import scala.swing.{FlowPanel, Button, TextArea, Label, ListView, Alignment, ScrollPane, Component, |
13 import scala.swing.{FlowPanel, Button, TextArea, Label, ListView, Alignment, |
14 BoxPanel, Orientation, RadioButton, ButtonGroup} |
14 ScrollPane, Component, CheckBox} |
15 import scala.swing.event.{ButtonClicked, MouseClicked} |
15 import scala.swing.event.{ButtonClicked, MouseClicked} |
16 |
16 |
17 import java.lang.System |
17 import java.lang.System |
18 import java.awt.{BorderLayout, Graphics2D, Insets} |
18 import java.awt.{BorderLayout, Graphics2D, Insets} |
19 import javax.swing.{JList, BorderFactory} |
19 import javax.swing.{JList, BorderFactory} |
53 private def handle_phase(phase: Session.Phase) |
53 private def handle_phase(phase: Session.Phase) |
54 { |
54 { |
55 Swing_Thread.later { session_phase.text = " " + phase_text(phase) + " " } |
55 Swing_Thread.later { session_phase.text = " " + phase_text(phase) + " " } |
56 } |
56 } |
57 |
57 |
58 private val execution_range = new BoxPanel(Orientation.Horizontal) { |
58 private val continuous_checking = new CheckBox("Continuous checking") { |
59 private def button(range: PIDE.Execution_Range.Value, tip: String): RadioButton = |
59 tooltip = "Continuous checking of proof document (visible and required parts)" |
60 new RadioButton(range.toString) { |
60 reactions += { case ButtonClicked(_) => PIDE.continuous_checking = selected } |
61 tooltip = tip |
61 def load() { selected = PIDE.continuous_checking } |
62 reactions += { case ButtonClicked(_) => PIDE.update_execution_range(range) } |
|
63 } |
|
64 private val label = |
|
65 new Label("Range:") { tooltip = "Execution range of continuous document processing" } |
|
66 private val b1 = button(PIDE.Execution_Range.ALL, "Check all theories (potentially slow)") |
|
67 private val b2 = button(PIDE.Execution_Range.NONE, "Check nothing") |
|
68 private val b3 = button(PIDE.Execution_Range.VISIBLE, "Check visible parts of theories") |
|
69 private val group = new ButtonGroup(b1, b2, b3) |
|
70 contents ++= List(label, b1, b2, b3) |
|
71 border = new SoftBevelBorder(BevelBorder.LOWERED) |
|
72 |
|
73 def load() |
|
74 { |
|
75 PIDE.execution_range() match { |
|
76 case PIDE.Execution_Range.ALL => group.select(b1) |
|
77 case PIDE.Execution_Range.NONE => group.select(b2) |
|
78 case PIDE.Execution_Range.VISIBLE => group.select(b3) |
|
79 } |
|
80 } |
|
81 load() |
62 load() |
82 } |
63 } |
83 |
64 |
84 private val logic = Isabelle_Logic.logic_selector(true) |
65 private val logic = Isabelle_Logic.logic_selector(true) |
85 |
66 |
86 private val controls = |
67 private val controls = |
87 new FlowPanel(FlowPanel.Alignment.Right)(execution_range, session_phase, logic) |
68 new FlowPanel(FlowPanel.Alignment.Right)(continuous_checking, session_phase, logic) |
88 add(controls.peer, BorderLayout.NORTH) |
69 add(controls.peer, BorderLayout.NORTH) |
89 |
70 |
90 |
71 |
91 /* component state -- owned by Swing thread */ |
72 /* component state -- owned by Swing thread */ |
92 |
73 |