# HG changeset patch # User wenzelm # Date 1670511902 -3600 # Node ID f10e6af0264fcdf179e74176998267ce66eecc62 # Parent b5dfe15516375545822bb84be463723e86615d71 clarified modules; diff -r b5dfe1551637 -r f10e6af0264f src/Tools/jEdit/src/theories_status.scala --- 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 =