9 |
9 |
10 import isabelle._ |
10 import isabelle._ |
11 |
11 |
12 import scala.swing.{Button, TextArea, Label, ListView, Alignment, |
12 import scala.swing.{Button, TextArea, Label, ListView, Alignment, |
13 ScrollPane, Component, CheckBox, BorderPanel} |
13 ScrollPane, Component, CheckBox, BorderPanel} |
14 import scala.swing.event.{MouseClicked, MouseMoved} |
14 import scala.swing.event.{ButtonClicked, MouseClicked, MouseMoved} |
15 |
15 |
16 import java.awt.{BorderLayout, Graphics2D, Color, Point, Dimension} |
16 import java.awt.{BorderLayout, Graphics2D, Color, Point, Dimension} |
17 import javax.swing.{JList, BorderFactory, UIManager} |
17 import javax.swing.{JList, BorderFactory, UIManager} |
18 import javax.swing.border.{BevelBorder, SoftBevelBorder} |
18 import javax.swing.border.{BevelBorder, SoftBevelBorder} |
19 |
19 |
70 { |
70 { |
71 GUI_Thread.require {} |
71 GUI_Thread.require {} |
72 session_phase.text = " " + phase_text(phase) + " " |
72 session_phase.text = " " + phase_text(phase) + " " |
73 } |
73 } |
74 |
74 |
|
75 private val purge = new Button("Purge") { |
|
76 tooltip = "Restrict document model to theories required for open editor buffers" |
|
77 reactions += { case ButtonClicked(_) => PIDE.editor.purge() } |
|
78 } |
|
79 |
75 private val continuous_checking = new Isabelle.Continuous_Checking |
80 private val continuous_checking = new Isabelle.Continuous_Checking |
76 continuous_checking.focusable = false |
81 continuous_checking.focusable = false |
77 |
82 |
78 private val logic = JEdit_Sessions.logic_selector(true) |
83 private val logic = JEdit_Sessions.logic_selector(true) |
79 |
84 |
80 private val controls = |
85 private val controls = |
81 new Wrap_Panel(Wrap_Panel.Alignment.Right)(continuous_checking, session_phase, logic) |
86 new Wrap_Panel(Wrap_Panel.Alignment.Right)(purge, continuous_checking, session_phase, logic) |
82 add(controls.peer, BorderLayout.NORTH) |
87 add(controls.peer, BorderLayout.NORTH) |
83 |
88 |
84 |
89 |
85 /* component state -- owned by GUI thread */ |
90 /* component state -- owned by GUI thread */ |
86 |
91 |