18 import javax.swing.border.{BevelBorder, SoftBevelBorder} |
18 import javax.swing.border.{BevelBorder, SoftBevelBorder} |
19 |
19 |
20 import org.gjt.sp.jedit.{View, jEdit} |
20 import org.gjt.sp.jedit.{View, jEdit} |
21 |
21 |
22 |
22 |
23 class Theories_Dockable(view: View, position: String) extends Dockable(view, position) |
23 class Theories_Dockable(view: View, position: String) extends Dockable(view, position) { |
24 { |
|
25 /* status */ |
24 /* status */ |
26 |
25 |
27 private val status = new ListView(List.empty[Document.Node.Name]) { |
26 private val status = new ListView(List.empty[Document.Node.Name]) { |
28 background = |
27 background = { |
29 { |
|
30 // enforce default value |
28 // enforce default value |
31 val c = UIManager.getDefaults.getColor("Panel.background") |
29 val c = UIManager.getDefaults.getColor("Panel.background") |
32 new Color(c.getRed, c.getGreen, c.getBlue, c.getAlpha) |
30 new Color(c.getRed, c.getGreen, c.getBlue, c.getAlpha) |
33 } |
31 } |
34 listenTo(mouse.clicks) |
32 listenTo(mouse.clicks) |
70 |
68 |
71 private val session_phase = new Label(phase_text(PIDE.session.phase)) |
69 private val session_phase = new Label(phase_text(PIDE.session.phase)) |
72 session_phase.border = new SoftBevelBorder(BevelBorder.LOWERED) |
70 session_phase.border = new SoftBevelBorder(BevelBorder.LOWERED) |
73 session_phase.tooltip = "Status of prover session" |
71 session_phase.tooltip = "Status of prover session" |
74 |
72 |
75 private def handle_phase(phase: Session.Phase): Unit = |
73 private def handle_phase(phase: Session.Phase): Unit = { |
76 { |
|
77 GUI_Thread.require {} |
74 GUI_Thread.require {} |
78 session_phase.text = " " + phase_text(phase) + " " |
75 session_phase.text = " " + phase_text(phase) + " " |
79 } |
76 } |
80 |
77 |
81 private val purge = new Button("Purge") { |
78 private val purge = new Button("Purge") { |
112 |
109 |
113 private def in_label(loc0: Point, p: Point): Boolean = |
110 private def in_label(loc0: Point, p: Point): Boolean = |
114 Node_Renderer_Component != null && in(Node_Renderer_Component.label_geometry, loc0, p) |
111 Node_Renderer_Component != null && in(Node_Renderer_Component.label_geometry, loc0, p) |
115 |
112 |
116 |
113 |
117 private object Node_Renderer_Component extends BorderPanel |
114 private object Node_Renderer_Component extends BorderPanel { |
118 { |
|
119 opaque = true |
115 opaque = true |
120 border = BorderFactory.createEmptyBorder(2, 2, 2, 2) |
116 border = BorderFactory.createEmptyBorder(2, 2, 2, 2) |
121 |
117 |
122 var node_name = Document.Node.Name.empty |
118 var node_name = Document.Node.Name.empty |
123 |
119 |
124 var checkbox_geometry: Option[(Point, Dimension)] = None |
120 var checkbox_geometry: Option[(Point, Dimension)] = None |
125 val checkbox = new CheckBox { |
121 val checkbox = new CheckBox { |
126 opaque = false |
122 opaque = false |
127 override def paintComponent(gfx: Graphics2D): Unit = |
123 override def paintComponent(gfx: Graphics2D): Unit = { |
128 { |
|
129 super.paintComponent(gfx) |
124 super.paintComponent(gfx) |
130 if (location != null && size != null) |
125 if (location != null && size != null) |
131 checkbox_geometry = Some((location, size)) |
126 checkbox_geometry = Some((location, size)) |
132 } |
127 } |
133 } |
128 } |
137 background = view.getTextArea.getPainter.getBackground |
132 background = view.getTextArea.getPainter.getBackground |
138 foreground = view.getTextArea.getPainter.getForeground |
133 foreground = view.getTextArea.getPainter.getForeground |
139 opaque = false |
134 opaque = false |
140 xAlignment = Alignment.Leading |
135 xAlignment = Alignment.Leading |
141 |
136 |
142 override def paintComponent(gfx: Graphics2D): Unit = |
137 override def paintComponent(gfx: Graphics2D): Unit = { |
143 { |
138 def paint_segment(x: Int, w: Int, color: Color): Unit = { |
144 def paint_segment(x: Int, w: Int, color: Color): Unit = |
|
145 { |
|
146 gfx.setColor(color) |
139 gfx.setColor(color) |
147 gfx.fillRect(x, 0, w, size.height) |
140 gfx.fillRect(x, 0, w, size.height) |
148 } |
141 } |
149 |
142 |
150 paint_segment(0, size.width, background) |
143 paint_segment(0, size.width, background) |
173 if (location != null && size != null) |
166 if (location != null && size != null) |
174 label_geometry = Some((location, size)) |
167 label_geometry = Some((location, size)) |
175 } |
168 } |
176 } |
169 } |
177 |
170 |
178 def label_border(name: Document.Node.Name): Unit = |
171 def label_border(name: Document.Node.Name): Unit = { |
179 { |
|
180 val st = nodes_status.overall_node_status(name) |
172 val st = nodes_status.overall_node_status(name) |
181 val color = |
173 val color = |
182 st match { |
174 st match { |
183 case Document_Status.Overall_Node_Status.ok => |
175 case Document_Status.Overall_Node_Status.ok => |
184 PIDE.options.color_value("ok_color") |
176 PIDE.options.color_value("ok_color") |
197 |
189 |
198 layout(checkbox) = BorderPanel.Position.West |
190 layout(checkbox) = BorderPanel.Position.West |
199 layout(label) = BorderPanel.Position.Center |
191 layout(label) = BorderPanel.Position.Center |
200 } |
192 } |
201 |
193 |
202 private class Node_Renderer extends ListView.Renderer[Document.Node.Name] |
194 private class Node_Renderer extends ListView.Renderer[Document.Node.Name] { |
203 { |
195 def componentFor( |
204 def componentFor(list: ListView[_ <: isabelle.Document.Node.Name], isSelected: Boolean, |
196 list: ListView[_ <: isabelle.Document.Node.Name], |
205 focused: Boolean, name: Document.Node.Name, index: Int): Component = |
197 isSelected: Boolean, |
206 { |
198 focused: Boolean, |
|
199 name: Document.Node.Name, |
|
200 index: Int |
|
201 ): Component = { |
207 val component = Node_Renderer_Component |
202 val component = Node_Renderer_Component |
208 component.node_name = name |
203 component.node_name = name |
209 component.checkbox.selected = nodes_required.contains(name) |
204 component.checkbox.selected = nodes_required.contains(name) |
210 component.label_border(name) |
205 component.label_border(name) |
211 component.label.text = name.theory_base_name |
206 component.label.text = name.theory_base_name |
213 } |
208 } |
214 } |
209 } |
215 status.renderer = new Node_Renderer |
210 status.renderer = new Node_Renderer |
216 |
211 |
217 private def handle_update( |
212 private def handle_update( |
218 domain: Option[Set[Document.Node.Name]] = None, trim: Boolean = false): Unit = |
213 domain: Option[Set[Document.Node.Name]] = None, |
219 { |
214 trim: Boolean = false |
|
215 ): Unit = { |
220 GUI_Thread.require {} |
216 GUI_Thread.require {} |
221 |
217 |
222 val snapshot = PIDE.session.snapshot() |
218 val snapshot = PIDE.session.snapshot() |
223 |
219 |
224 val (nodes_status_changed, nodes_status1) = |
220 val (nodes_status_changed, nodes_status1) = |
253 |
249 |
254 case changed: Session.Commands_Changed => |
250 case changed: Session.Commands_Changed => |
255 GUI_Thread.later { handle_update(domain = Some(changed.nodes), trim = changed.assignment) } |
251 GUI_Thread.later { handle_update(domain = Some(changed.nodes), trim = changed.assignment) } |
256 } |
252 } |
257 |
253 |
258 override def init(): Unit = |
254 override def init(): Unit = { |
259 { |
|
260 PIDE.session.phase_changed += main |
255 PIDE.session.phase_changed += main |
261 PIDE.session.global_options += main |
256 PIDE.session.global_options += main |
262 PIDE.session.commands_changed += main |
257 PIDE.session.commands_changed += main |
263 |
258 |
264 handle_phase(PIDE.session.phase) |
259 handle_phase(PIDE.session.phase) |
265 handle_update() |
260 handle_update() |
266 } |
261 } |
267 |
262 |
268 override def exit(): Unit = |
263 override def exit(): Unit = { |
269 { |
|
270 PIDE.session.phase_changed -= main |
264 PIDE.session.phase_changed -= main |
271 PIDE.session.global_options -= main |
265 PIDE.session.global_options -= main |
272 PIDE.session.commands_changed -= main |
266 PIDE.session.commands_changed -= main |
273 } |
267 } |
274 } |
268 } |