author | wenzelm |
Sun, 05 Feb 2023 15:59:18 +0100 | |
changeset 77197 | a541da01ba67 |
parent 77161 | 913c781ff6ba |
child 78600 | afb83ba8d24c |
permissions | -rw-r--r-- |
76566 | 1 |
/* Title: Tools/jEdit/src/theories_status.scala |
2 |
Author: Makarius |
|
3 |
||
4 |
GUI panel for status of theories. |
|
5 |
*/ |
|
6 |
||
7 |
package isabelle.jedit |
|
8 |
||
9 |
||
10 |
import isabelle._ |
|
11 |
||
12 |
import scala.swing.{ListView, Alignment, Label, CheckBox, BorderPanel, BoxPanel, Orientation, |
|
13 |
Component} |
|
14 |
import scala.swing.event.{MouseClicked, MouseMoved} |
|
15 |
||
16 |
import java.awt.{BorderLayout, Graphics2D, Color, Point, Dimension} |
|
17 |
import javax.swing.border.{BevelBorder, SoftBevelBorder} |
|
18 |
import javax.swing.{JList, BorderFactory, UIManager} |
|
19 |
||
20 |
import org.gjt.sp.jedit.View |
|
21 |
||
22 |
||
76602 | 23 |
class Theories_Status(view: View, document: Boolean = false) { |
76566 | 24 |
/* component state -- owned by GUI thread */ |
25 |
||
26 |
private var nodes_status = Document_Status.Nodes_Status.empty |
|
76716
a7602257a825
clarified state document nodes for Theories_Status / Document_Dockable;
wenzelm
parents:
76715
diff
changeset
|
27 |
private var nodes_required = Set.empty[Document.Node.Name] |
76713 | 28 |
private var document_required = Set.empty[Document.Node.Name] |
29 |
||
77161
913c781ff6ba
support document preparation from already loaded theories;
wenzelm
parents:
76719
diff
changeset
|
30 |
private def is_loaded_theory(name: Document.Node.Name): Boolean = |
913c781ff6ba
support document preparation from already loaded theories;
wenzelm
parents:
76719
diff
changeset
|
31 |
PIDE.resources.session_base.loaded_theory(name) |
913c781ff6ba
support document preparation from already loaded theories;
wenzelm
parents:
76719
diff
changeset
|
32 |
|
913c781ff6ba
support document preparation from already loaded theories;
wenzelm
parents:
76719
diff
changeset
|
33 |
private def overall_node_status( |
913c781ff6ba
support document preparation from already loaded theories;
wenzelm
parents:
76719
diff
changeset
|
34 |
name: Document.Node.Name |
913c781ff6ba
support document preparation from already loaded theories;
wenzelm
parents:
76719
diff
changeset
|
35 |
): Document_Status.Overall_Node_Status.Value = { |
913c781ff6ba
support document preparation from already loaded theories;
wenzelm
parents:
76719
diff
changeset
|
36 |
if (is_loaded_theory(name)) Document_Status.Overall_Node_Status.ok |
913c781ff6ba
support document preparation from already loaded theories;
wenzelm
parents:
76719
diff
changeset
|
37 |
else nodes_status.overall_node_status(name) |
913c781ff6ba
support document preparation from already loaded theories;
wenzelm
parents:
76719
diff
changeset
|
38 |
} |
913c781ff6ba
support document preparation from already loaded theories;
wenzelm
parents:
76719
diff
changeset
|
39 |
|
76713 | 40 |
private def init_state(): Unit = GUI_Thread.require { |
76716
a7602257a825
clarified state document nodes for Theories_Status / Document_Dockable;
wenzelm
parents:
76715
diff
changeset
|
41 |
if (document) { |
a7602257a825
clarified state document nodes for Theories_Status / Document_Dockable;
wenzelm
parents:
76715
diff
changeset
|
42 |
nodes_required = PIDE.editor.document_required().toSet |
a7602257a825
clarified state document nodes for Theories_Status / Document_Dockable;
wenzelm
parents:
76715
diff
changeset
|
43 |
} |
a7602257a825
clarified state document nodes for Theories_Status / Document_Dockable;
wenzelm
parents:
76715
diff
changeset
|
44 |
else { |
a7602257a825
clarified state document nodes for Theories_Status / Document_Dockable;
wenzelm
parents:
76715
diff
changeset
|
45 |
nodes_required = Document_Model.nodes_required() |
a7602257a825
clarified state document nodes for Theories_Status / Document_Dockable;
wenzelm
parents:
76715
diff
changeset
|
46 |
document_required = PIDE.editor.document_required().toSet |
a7602257a825
clarified state document nodes for Theories_Status / Document_Dockable;
wenzelm
parents:
76715
diff
changeset
|
47 |
} |
76713 | 48 |
} |
76566 | 49 |
|
50 |
||
51 |
/* node renderer */ |
|
52 |
||
53 |
private class Geometry { |
|
54 |
private var location: Point = null |
|
55 |
private var size: Dimension = null |
|
56 |
||
57 |
def in(location0: Point, p: Point): Boolean = |
|
58 |
location != null && size != null && location0 != null && p != null && { |
|
59 |
val x = location0.x + location.x |
|
60 |
val y = location0.y + location.y |
|
61 |
x <= p.x && p.x < x + size.width && |
|
62 |
y <= p.y && p.y < y + size.height |
|
63 |
} |
|
64 |
||
65 |
def update(new_location: Point, new_size: Dimension): Unit = { |
|
66 |
if (new_location != null && new_size != null) { |
|
67 |
location = new_location |
|
68 |
size = new_size |
|
69 |
} |
|
70 |
} |
|
71 |
} |
|
72 |
||
76603 | 73 |
private class Node_Renderer extends ListView.Renderer[Document.Node.Name] { |
76710 | 74 |
private val document_marker = Symbol.decode(" \\<^file>") |
75 |
private val no_document_marker = " " |
|
76 |
||
76603 | 77 |
private object component extends BorderPanel { |
78 |
opaque = true |
|
79 |
border = BorderFactory.createEmptyBorder(2, 2, 2, 2) |
|
80 |
||
81 |
var node_name: Document.Node.Name = Document.Node.Name.empty |
|
76566 | 82 |
|
76603 | 83 |
val required_geometry = new Geometry |
76608 | 84 |
val required: CheckBox = new CheckBox { |
76603 | 85 |
opaque = false |
86 |
override def paintComponent(gfx: Graphics2D): Unit = { |
|
87 |
super.paintComponent(gfx) |
|
88 |
required_geometry.update(location, size) |
|
89 |
} |
|
90 |
} |
|
91 |
||
92 |
val label_geometry = new Geometry |
|
93 |
val label: Label = new Label { |
|
94 |
background = view.getTextArea.getPainter.getBackground |
|
95 |
foreground = view.getTextArea.getPainter.getForeground |
|
96 |
opaque = false |
|
97 |
xAlignment = Alignment.Leading |
|
98 |
||
99 |
override def paintComponent(gfx: Graphics2D): Unit = { |
|
100 |
def paint_segment(x: Int, w: Int, color: Color): Unit = { |
|
101 |
gfx.setColor(color) |
|
102 |
gfx.fillRect(x, 0, w, size.height) |
|
103 |
} |
|
76566 | 104 |
|
76603 | 105 |
paint_segment(0, size.width, background) |
106 |
nodes_status.get(node_name) match { |
|
107 |
case Some(node_status) => |
|
108 |
val segments = |
|
109 |
List( |
|
110 |
(node_status.unprocessed, PIDE.options.color_value("unprocessed1_color")), |
|
111 |
(node_status.running, PIDE.options.color_value("running_color")), |
|
112 |
(node_status.warned, PIDE.options.color_value("warning_color")), |
|
113 |
(node_status.failed, PIDE.options.color_value("error_color")) |
|
114 |
).filter(_._1 > 0) |
|
115 |
||
116 |
segments.foldLeft(size.width - 2) { |
|
117 |
case (last, (n, color)) => |
|
118 |
val w = (n * ((size.width - 4) - segments.length) / node_status.total) max 4 |
|
119 |
paint_segment(last - w, w, color) |
|
120 |
last - w - 1 |
|
121 |
} |
|
122 |
||
123 |
case None => |
|
77161
913c781ff6ba
support document preparation from already loaded theories;
wenzelm
parents:
76719
diff
changeset
|
124 |
if (!is_loaded_theory(node_name)) { |
913c781ff6ba
support document preparation from already loaded theories;
wenzelm
parents:
76719
diff
changeset
|
125 |
paint_segment(0, size.width, PIDE.options.color_value("unprocessed1_color")) |
913c781ff6ba
support document preparation from already loaded theories;
wenzelm
parents:
76719
diff
changeset
|
126 |
} |
76603 | 127 |
} |
128 |
super.paintComponent(gfx) |
|
129 |
||
130 |
label_geometry.update(location, size) |
|
131 |
} |
|
76602 | 132 |
} |
76603 | 133 |
|
134 |
def label_border(name: Document.Node.Name): Unit = { |
|
77161
913c781ff6ba
support document preparation from already loaded theories;
wenzelm
parents:
76719
diff
changeset
|
135 |
val st = overall_node_status(name) |
76603 | 136 |
val color = |
137 |
st match { |
|
138 |
case Document_Status.Overall_Node_Status.ok => |
|
139 |
PIDE.options.color_value("ok_color") |
|
140 |
case Document_Status.Overall_Node_Status.failed => |
|
141 |
PIDE.options.color_value("failed_color") |
|
142 |
case _ => label.foreground |
|
143 |
} |
|
144 |
val thickness1 = if (st == Document_Status.Overall_Node_Status.pending) 1 else 3 |
|
145 |
val thickness2 = 4 - thickness1 |
|
146 |
||
147 |
label.border = |
|
148 |
BorderFactory.createCompoundBorder( |
|
149 |
BorderFactory.createLineBorder(color, thickness1), |
|
150 |
BorderFactory.createEmptyBorder(thickness2, thickness2, thickness2, thickness2)) |
|
151 |
} |
|
152 |
||
153 |
layout(required) = BorderPanel.Position.West |
|
154 |
layout(label) = BorderPanel.Position.Center |
|
76602 | 155 |
} |
76566 | 156 |
|
76603 | 157 |
def in_required(location0: Point, p: Point): Boolean = |
158 |
component.required_geometry.in(location0, p) |
|
76566 | 159 |
|
76603 | 160 |
def in_label(location0: Point, p: Point): Boolean = |
161 |
component.label_geometry.in(location0, p) |
|
76566 | 162 |
|
163 |
def componentFor( |
|
164 |
list: ListView[_ <: isabelle.Document.Node.Name], |
|
165 |
isSelected: Boolean, |
|
166 |
focused: Boolean, |
|
167 |
name: Document.Node.Name, |
|
168 |
index: Int |
|
169 |
): Component = { |
|
170 |
component.node_name = name |
|
76716
a7602257a825
clarified state document nodes for Theories_Status / Document_Dockable;
wenzelm
parents:
76715
diff
changeset
|
171 |
component.required.selected = nodes_required.contains(name) |
76566 | 172 |
component.label_border(name) |
76710 | 173 |
component.label.text = |
174 |
name.theory_base_name + |
|
76716
a7602257a825
clarified state document nodes for Theories_Status / Document_Dockable;
wenzelm
parents:
76715
diff
changeset
|
175 |
(if (document_required.contains(name)) document_marker else no_document_marker) |
76566 | 176 |
component |
177 |
} |
|
178 |
} |
|
179 |
||
180 |
||
181 |
/* GUI component */ |
|
182 |
||
183 |
val gui: ListView[Document.Node.Name] = new ListView[Document.Node.Name](Nil) { |
|
76603 | 184 |
private val node_renderer = new Node_Renderer |
185 |
renderer = node_renderer |
|
186 |
||
76566 | 187 |
background = { |
188 |
// enforce default value |
|
189 |
val c = UIManager.getDefaults.getColor("Panel.background") |
|
190 |
new Color(c.getRed, c.getGreen, c.getBlue, c.getAlpha) |
|
191 |
} |
|
192 |
listenTo(mouse.clicks) |
|
193 |
listenTo(mouse.moves) |
|
194 |
reactions += { |
|
195 |
case MouseClicked(_, point, _, clicks, _) => |
|
196 |
val index = peer.locationToIndex(point) |
|
197 |
if (index >= 0) { |
|
198 |
val index_location = peer.indexToLocation(index) |
|
76603 | 199 |
if (node_renderer.in_required(index_location, point)) { |
76566 | 200 |
if (clicks == 1) { |
76715
bf5ff407f32f
clarified state of document model vs. document editor selection (again, see also a9d52d02bd83);
wenzelm
parents:
76713
diff
changeset
|
201 |
val name = listData(index) |
77197
a541da01ba67
clarified signature selection: SortedSet[String], which fits better to stored json and works properly on Windows (NB: document theories have an authentic session-theory name);
wenzelm
parents:
77161
diff
changeset
|
202 |
if (document) PIDE.editor.document_select(Set(name.theory), toggle = true) |
76715
bf5ff407f32f
clarified state of document model vs. document editor selection (again, see also a9d52d02bd83);
wenzelm
parents:
76713
diff
changeset
|
203 |
else Document_Model.node_required(name, toggle = true) |
76566 | 204 |
} |
205 |
} |
|
206 |
else if (clicks == 2) PIDE.editor.goto_file(true, view, listData(index).node) |
|
207 |
} |
|
208 |
case MouseMoved(_, point, _) => |
|
209 |
val index = peer.locationToIndex(point) |
|
210 |
val index_location = peer.indexToLocation(index) |
|
76603 | 211 |
if (index >= 0 && node_renderer.in_required(index_location, point)) { |
76602 | 212 |
tooltip = |
213 |
if (document) "Mark for inclusion in document" |
|
214 |
else "Mark as required for continuous checking" |
|
76566 | 215 |
} |
76603 | 216 |
else if (index >= 0 && node_renderer.in_label(index_location, point)) { |
76566 | 217 |
val name = listData(index) |
77161
913c781ff6ba
support document preparation from already loaded theories;
wenzelm
parents:
76719
diff
changeset
|
218 |
val st = overall_node_status(name) |
76566 | 219 |
tooltip = |
220 |
"theory " + quote(name.theory) + |
|
221 |
(if (st == Document_Status.Overall_Node_Status.ok) "" else " (" + st + ")") |
|
222 |
} |
|
223 |
else tooltip = null |
|
224 |
} |
|
76598 | 225 |
|
226 |
peer.setLayoutOrientation(JList.HORIZONTAL_WRAP) |
|
227 |
peer.setVisibleRowCount(0) |
|
228 |
selection.intervalMode = ListView.IntervalMode.Single |
|
76566 | 229 |
} |
230 |
||
231 |
||
232 |
/* update */ |
|
233 |
||
76716
a7602257a825
clarified state document nodes for Theories_Status / Document_Dockable;
wenzelm
parents:
76715
diff
changeset
|
234 |
def update( |
a7602257a825
clarified state document nodes for Theories_Status / Document_Dockable;
wenzelm
parents:
76715
diff
changeset
|
235 |
domain: Option[Set[Document.Node.Name]] = None, |
a7602257a825
clarified state document nodes for Theories_Status / Document_Dockable;
wenzelm
parents:
76715
diff
changeset
|
236 |
trim: Boolean = false, |
a7602257a825
clarified state document nodes for Theories_Status / Document_Dockable;
wenzelm
parents:
76715
diff
changeset
|
237 |
force: Boolean = false |
a7602257a825
clarified state document nodes for Theories_Status / Document_Dockable;
wenzelm
parents:
76715
diff
changeset
|
238 |
): Unit = { |
76566 | 239 |
GUI_Thread.require {} |
240 |
||
241 |
val snapshot = PIDE.session.snapshot() |
|
242 |
||
243 |
val (nodes_status_changed, nodes_status1) = |
|
244 |
nodes_status.update( |
|
245 |
PIDE.resources, snapshot.state, snapshot.version, domain = domain, trim = trim) |
|
246 |
||
247 |
nodes_status = nodes_status1 |
|
76716
a7602257a825
clarified state document nodes for Theories_Status / Document_Dockable;
wenzelm
parents:
76715
diff
changeset
|
248 |
if (nodes_status_changed || force) { |
76566 | 249 |
gui.listData = |
76719 | 250 |
if (document) { |
251 |
nodes_status1.present(domain = Some(PIDE.editor.document_theories())).map(_._1) |
|
252 |
} |
|
76716
a7602257a825
clarified state document nodes for Theories_Status / Document_Dockable;
wenzelm
parents:
76715
diff
changeset
|
253 |
else { |
a7602257a825
clarified state document nodes for Theories_Status / Document_Dockable;
wenzelm
parents:
76715
diff
changeset
|
254 |
(for { |
a7602257a825
clarified state document nodes for Theories_Status / Document_Dockable;
wenzelm
parents:
76715
diff
changeset
|
255 |
(name, node_status) <- nodes_status1.present().iterator |
a7602257a825
clarified state document nodes for Theories_Status / Document_Dockable;
wenzelm
parents:
76715
diff
changeset
|
256 |
if !node_status.is_empty && !node_status.is_suppressed && node_status.total > 0 |
a7602257a825
clarified state document nodes for Theories_Status / Document_Dockable;
wenzelm
parents:
76715
diff
changeset
|
257 |
} yield name).toList |
a7602257a825
clarified state document nodes for Theories_Status / Document_Dockable;
wenzelm
parents:
76715
diff
changeset
|
258 |
} |
76566 | 259 |
} |
260 |
} |
|
261 |
||
262 |
||
76711 | 263 |
/* refresh */ |
76566 | 264 |
|
76713 | 265 |
def refresh(): Unit = GUI_Thread.require { |
266 |
init_state() |
|
76566 | 267 |
gui.repaint() |
268 |
} |
|
76713 | 269 |
|
270 |
init_state() |
|
76566 | 271 |
} |