--- a/src/Tools/jEdit/src/theories_status.scala Thu Dec 08 14:02:59 2022 +0100
+++ b/src/Tools/jEdit/src/theories_status.scala Thu Dec 08 16:05:02 2022 +0100
@@ -50,91 +50,91 @@
}
}
- private object Node_Renderer_Component extends BorderPanel {
- opaque = true
- border = BorderFactory.createEmptyBorder(2, 2, 2, 2)
+ private class Node_Renderer extends ListView.Renderer[Document.Node.Name] {
+ private object component extends BorderPanel {
+ opaque = true
+ border = BorderFactory.createEmptyBorder(2, 2, 2, 2)
+
+ var node_name: Document.Node.Name = Document.Node.Name.empty
- var node_name: Document.Node.Name = Document.Node.Name.empty
+ val required_geometry = new Geometry
+ val required = new CheckBox {
+ opaque = false
+ override def paintComponent(gfx: Graphics2D): Unit = {
+ super.paintComponent(gfx)
+ required_geometry.update(location, size)
+ }
+ }
+
+ val label_geometry = new Geometry
+ val label: Label = new Label {
+ background = view.getTextArea.getPainter.getBackground
+ foreground = view.getTextArea.getPainter.getForeground
+ opaque = false
+ xAlignment = Alignment.Leading
+
+ override def paintComponent(gfx: Graphics2D): Unit = {
+ def paint_segment(x: Int, w: Int, color: Color): Unit = {
+ gfx.setColor(color)
+ gfx.fillRect(x, 0, w, size.height)
+ }
- val required_geometry = new Geometry
- val required = new CheckBox {
- opaque = false
- override def paintComponent(gfx: Graphics2D): Unit = {
- super.paintComponent(gfx)
- required_geometry.update(location, size)
+ paint_segment(0, size.width, background)
+ nodes_status.get(node_name) match {
+ case Some(node_status) =>
+ val segments =
+ List(
+ (node_status.unprocessed, PIDE.options.color_value("unprocessed1_color")),
+ (node_status.running, PIDE.options.color_value("running_color")),
+ (node_status.warned, PIDE.options.color_value("warning_color")),
+ (node_status.failed, PIDE.options.color_value("error_color"))
+ ).filter(_._1 > 0)
+
+ segments.foldLeft(size.width - 2) {
+ case (last, (n, color)) =>
+ val w = (n * ((size.width - 4) - segments.length) / node_status.total) max 4
+ paint_segment(last - w, w, color)
+ last - w - 1
+ }
+
+ case None =>
+ paint_segment(0, size.width, PIDE.options.color_value("unprocessed1_color"))
+ }
+ super.paintComponent(gfx)
+
+ label_geometry.update(location, size)
+ }
}
+
+ def label_border(name: Document.Node.Name): Unit = {
+ val st = nodes_status.overall_node_status(name)
+ val color =
+ st match {
+ case Document_Status.Overall_Node_Status.ok =>
+ PIDE.options.color_value("ok_color")
+ case Document_Status.Overall_Node_Status.failed =>
+ PIDE.options.color_value("failed_color")
+ case _ => label.foreground
+ }
+ val thickness1 = if (st == Document_Status.Overall_Node_Status.pending) 1 else 3
+ val thickness2 = 4 - thickness1
+
+ label.border =
+ BorderFactory.createCompoundBorder(
+ BorderFactory.createLineBorder(color, thickness1),
+ BorderFactory.createEmptyBorder(thickness2, thickness2, thickness2, thickness2))
+ }
+
+ layout(required) = BorderPanel.Position.West
+ layout(label) = BorderPanel.Position.Center
}
- val label_geometry = new Geometry
- val label: Label = new Label {
- background = view.getTextArea.getPainter.getBackground
- foreground = view.getTextArea.getPainter.getForeground
- opaque = false
- xAlignment = Alignment.Leading
-
- override def paintComponent(gfx: Graphics2D): Unit = {
- def paint_segment(x: Int, w: Int, color: Color): Unit = {
- gfx.setColor(color)
- gfx.fillRect(x, 0, w, size.height)
- }
-
- paint_segment(0, size.width, background)
- nodes_status.get(node_name) match {
- case Some(node_status) =>
- val segments =
- List(
- (node_status.unprocessed, PIDE.options.color_value("unprocessed1_color")),
- (node_status.running, PIDE.options.color_value("running_color")),
- (node_status.warned, PIDE.options.color_value("warning_color")),
- (node_status.failed, PIDE.options.color_value("error_color"))
- ).filter(_._1 > 0)
-
- segments.foldLeft(size.width - 2) {
- case (last, (n, color)) =>
- val w = (n * ((size.width - 4) - segments.length) / node_status.total) max 4
- paint_segment(last - w, w, color)
- last - w - 1
- }
+ def in_required(location0: Point, p: Point): Boolean =
+ component.required_geometry.in(location0, p)
- case None =>
- paint_segment(0, size.width, PIDE.options.color_value("unprocessed1_color"))
- }
- super.paintComponent(gfx)
-
- label_geometry.update(location, size)
- }
- }
+ def in_label(location0: Point, p: Point): Boolean =
+ component.label_geometry.in(location0, p)
- def label_border(name: Document.Node.Name): Unit = {
- val st = nodes_status.overall_node_status(name)
- val color =
- st match {
- case Document_Status.Overall_Node_Status.ok =>
- PIDE.options.color_value("ok_color")
- case Document_Status.Overall_Node_Status.failed =>
- PIDE.options.color_value("failed_color")
- case _ => label.foreground
- }
- val thickness1 = if (st == Document_Status.Overall_Node_Status.pending) 1 else 3
- val thickness2 = 4 - thickness1
-
- label.border =
- BorderFactory.createCompoundBorder(
- BorderFactory.createLineBorder(color, thickness1),
- BorderFactory.createEmptyBorder(thickness2, thickness2, thickness2, thickness2))
- }
-
- layout(required) = BorderPanel.Position.West
- layout(label) = BorderPanel.Position.Center
- }
-
- private def in_required(location0: Point, p: Point): Boolean =
- Node_Renderer_Component != null && Node_Renderer_Component.required_geometry.in(location0, p)
-
- private def in_label(location0: Point, p: Point): Boolean =
- Node_Renderer_Component != null && Node_Renderer_Component.label_geometry.in(location0, p)
-
- private class Node_Renderer extends ListView.Renderer[Document.Node.Name] {
def componentFor(
list: ListView[_ <: isabelle.Document.Node.Name],
isSelected: Boolean,
@@ -142,7 +142,6 @@
name: Document.Node.Name,
index: Int
): Component = {
- val component = Node_Renderer_Component
component.node_name = name
component.required.selected =
(if (document) document_required else theory_required).contains(name)
@@ -156,7 +155,9 @@
/* GUI component */
val gui: ListView[Document.Node.Name] = new ListView[Document.Node.Name](Nil) {
- renderer = new Node_Renderer
+ private val node_renderer = new Node_Renderer
+ renderer = node_renderer
+
background = {
// enforce default value
val c = UIManager.getDefaults.getColor("Panel.background")
@@ -169,7 +170,7 @@
val index = peer.locationToIndex(point)
if (index >= 0) {
val index_location = peer.indexToLocation(index)
- if (in_required(index_location, point)) {
+ if (node_renderer.in_required(index_location, point)) {
if (clicks == 1) {
Document_Model.node_required(listData(index), toggle = true, document = document)
}
@@ -179,12 +180,12 @@
case MouseMoved(_, point, _) =>
val index = peer.locationToIndex(point)
val index_location = peer.indexToLocation(index)
- if (index >= 0 && in_required(index_location, point)) {
+ if (index >= 0 && node_renderer.in_required(index_location, point)) {
tooltip =
if (document) "Mark for inclusion in document"
else "Mark as required for continuous checking"
}
- else if (index >= 0 && in_label(index_location, point)) {
+ else if (index >= 0 && node_renderer.in_label(index_location, point)) {
val name = listData(index)
val st = nodes_status.overall_node_status(name)
tooltip =