# HG changeset patch # User wenzelm # Date 1670271039 -3600 # Node ID 318c6b466ec05087a3f6e98184d3bc150593a517 # Parent 6827dd0c372319a8cb281eebadd7c84a75f5ee92 clarified modules; diff -r 6827dd0c3723 -r 318c6b466ec0 etc/build.props --- a/etc/build.props Mon Dec 05 16:27:27 2022 +0100 +++ b/etc/build.props Mon Dec 05 21:10:39 2022 +0100 @@ -297,6 +297,7 @@ src/Tools/jEdit/src/text_overview.scala \ src/Tools/jEdit/src/text_structure.scala \ src/Tools/jEdit/src/theories_dockable.scala \ + src/Tools/jEdit/src/theories_status.scala \ src/Tools/jEdit/src/timing_dockable.scala \ src/Tools/jEdit/src/token_markup.scala services = \ diff -r 6827dd0c3723 -r 318c6b466ec0 src/Tools/jEdit/src/theories_dockable.scala --- a/src/Tools/jEdit/src/theories_dockable.scala Mon Dec 05 16:27:27 2022 +0100 +++ b/src/Tools/jEdit/src/theories_dockable.scala Mon Dec 05 21:10:39 2022 +0100 @@ -9,68 +9,15 @@ import isabelle._ -import scala.swing.{Button, TextArea, Label, ListView, Alignment, - ScrollPane, Component, CheckBox, BorderPanel, BoxPanel, Orientation} -import scala.swing.event.{MouseClicked, MouseMoved} +import scala.swing.{Button, TextArea, Label, ListView, ScrollPane, Component} import java.awt.{BorderLayout, Graphics2D, Color, Point, Dimension} -import javax.swing.{JList, BorderFactory, UIManager} import javax.swing.border.{BevelBorder, SoftBevelBorder} import org.gjt.sp.jedit.{View, jEdit} class Theories_Dockable(view: View, position: String) extends Dockable(view, position) { - /* status */ - - private val status = new ListView[Document.Node.Name](Nil) { - background = { - // enforce default value - val c = UIManager.getDefaults.getColor("Panel.background") - new Color(c.getRed, c.getGreen, c.getBlue, c.getAlpha) - } - listenTo(mouse.clicks) - listenTo(mouse.moves) - reactions += { - case MouseClicked(_, point, _, clicks, _) => - val index = peer.locationToIndex(point) - if (index >= 0) { - val index_location = peer.indexToLocation(index) - val a = in_required(index_location, point) - val b = in_required(index_location, point, document = true) - if (a || b) { - if (clicks == 1) { - Document_Model.node_required(listData(index), toggle = true, document = b) - } - } - else if (clicks == 2) PIDE.editor.goto_file(true, view, listData(index).node) - } - case MouseMoved(_, point, _) => - val index = peer.locationToIndex(point) - val index_location = peer.indexToLocation(index) - if (index >= 0 && in_required(index_location, point)) { - tooltip = "Mark as required for continuous checking" - } - else if (index >= 0 && in_required(index_location, point, document = true)) { - tooltip = "Mark as required for continuous checking, with inclusion in document" - } - else if (index >= 0 && in_label(index_location, point)) { - val name = listData(index) - val st = nodes_status.overall_node_status(name) - tooltip = - "theory " + quote(name.theory) + - (if (st == Document_Status.Overall_Node_Status.ok) "" else " (" + st + ")") - } - else tooltip = null - } - } - status.peer.setLayoutOrientation(JList.HORIZONTAL_WRAP) - status.peer.setVisibleRowCount(0) - status.selection.intervalMode = ListView.IntervalMode.Single - - set_content(new ScrollPane(status)) - - /* controls */ def phase_text(phase: Session.Phase): String = "Prover: " + phase.print @@ -79,8 +26,7 @@ session_phase.border = new SoftBevelBorder(BevelBorder.LOWERED) session_phase.tooltip = "Status of prover session" - private def handle_phase(phase: Session.Phase): Unit = { - GUI_Thread.require {} + private def handle_phase(phase: Session.Phase): Unit = GUI_Thread.require { session_phase.text = " " + phase_text(phase) + " " } @@ -100,171 +46,10 @@ add(controls.peer, BorderLayout.NORTH) - /* component state -- owned by GUI thread */ - - private var nodes_status = Document_Status.Nodes_Status.empty - private var theory_required: Set[Document.Node.Name] = Document_Model.required_nodes(false) - private var document_required: Set[Document.Node.Name] = Document_Model.required_nodes(true) - - private class Geometry { - private var location: Point = null - private var size: Dimension = null - - def in(location0: Point, p: Point): Boolean = - location != null && size != null && location0 != null && p != null && { - val x = location0.x + location.x - val y = location0.y + location.y - x <= p.x && p.x < x + size.width && - y <= p.y && p.y < y + size.height - } - - def update(new_location: Point, new_size: Dimension): Unit = { - if (new_location != null && new_size != null) { - location = new_location - size = new_size - } - } - } - - private def in_required(location0: Point, p: Point, document: Boolean = false): Boolean = - Node_Renderer_Component != null && { - val required = - if (document) Node_Renderer_Component.document_required - else Node_Renderer_Component.theory_required - 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 Required extends CheckBox { - val geometry = new Geometry - opaque = false - override def paintComponent(gfx: Graphics2D): Unit = { - super.paintComponent(gfx) - geometry.update(location, size) - } - } - - private object Node_Renderer_Component extends BorderPanel { - opaque = true - border = BorderFactory.createEmptyBorder(2, 2, 2, 2) - - var node_name: Document.Node.Name = Document.Node.Name.empty - - val theory_required = new Required - val document_required = new Required - - 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) + /* main */ - 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)) - } - - val required = new BoxPanel(Orientation.Horizontal) - required.contents += theory_required - // FIXME required.contents += document_required - - layout(required) = BorderPanel.Position.West - layout(label) = BorderPanel.Position.Center - } - - private class Node_Renderer extends ListView.Renderer[Document.Node.Name] { - def componentFor( - list: ListView[_ <: isabelle.Document.Node.Name], - isSelected: Boolean, - focused: Boolean, - name: Document.Node.Name, - index: Int - ): Component = { - val component = Node_Renderer_Component - component.node_name = name - component.theory_required.selected = theory_required.contains(name) - component.document_required.selected = document_required.contains(name) - component.label_border(name) - component.label.text = name.theory_base_name - component - } - } - status.renderer = new Node_Renderer - - private def handle_update( - domain: Option[Set[Document.Node.Name]] = None, - trim: Boolean = false - ): Unit = { - GUI_Thread.require {} - - val snapshot = PIDE.session.snapshot() - - val (nodes_status_changed, nodes_status1) = - nodes_status.update( - PIDE.resources, snapshot.state, snapshot.version, domain = domain, trim = trim) - - nodes_status = nodes_status1 - if (nodes_status_changed) { - status.listData = - (for { - (name, node_status) <- nodes_status1.present.iterator - if !node_status.is_suppressed && node_status.total > 0 - } yield name).toList - } - } - - - /* main */ + val status = new Theories_Status(view) + set_content(new ScrollPane(status.gui)) private val main = Session.Consumer[Any](getClass.getName) { @@ -274,14 +59,12 @@ case _: Session.Global_Options => GUI_Thread.later { continuous_checking.load() - logic.load () - theory_required = Document_Model.required_nodes(false) - document_required = Document_Model.required_nodes(true) - status.repaint() + logic.load() + status.reinit() } case changed: Session.Commands_Changed => - GUI_Thread.later { handle_update(domain = Some(changed.nodes), trim = changed.assignment) } + GUI_Thread.later { status.update(domain = Some(changed.nodes), trim = changed.assignment) } } override def init(): Unit = { @@ -290,7 +73,7 @@ PIDE.session.commands_changed += main handle_phase(PIDE.session.phase) - handle_update() + status.update() } override def exit(): Unit = { diff -r 6827dd0c3723 -r 318c6b466ec0 src/Tools/jEdit/src/theories_status.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/src/theories_status.scala Mon Dec 05 21:10:39 2022 +0100 @@ -0,0 +1,249 @@ +/* Title: Tools/jEdit/src/theories_status.scala + Author: Makarius + +GUI panel for status of theories. +*/ + +package isabelle.jedit + + +import isabelle._ + +import scala.swing.{ListView, Alignment, Label, CheckBox, BorderPanel, BoxPanel, Orientation, + Component} +import scala.swing.event.{MouseClicked, MouseMoved} + +import java.awt.{BorderLayout, Graphics2D, Color, Point, Dimension} +import javax.swing.border.{BevelBorder, SoftBevelBorder} +import javax.swing.{JList, BorderFactory, UIManager} + +import org.gjt.sp.jedit.View + + +class Theories_Status(view: View) { + /* component state -- owned by GUI thread */ + + private var nodes_status = Document_Status.Nodes_Status.empty + private var theory_required: Set[Document.Node.Name] = Document_Model.required_nodes(false) + private var document_required: Set[Document.Node.Name] = Document_Model.required_nodes(true) + + + /* node renderer */ + + private class Geometry { + private var location: Point = null + private var size: Dimension = null + + def in(location0: Point, p: Point): Boolean = + location != null && size != null && location0 != null && p != null && { + val x = location0.x + location.x + val y = location0.y + location.y + x <= p.x && p.x < x + size.width && + y <= p.y && p.y < y + size.height + } + + def update(new_location: Point, new_size: Dimension): Unit = { + if (new_location != null && new_size != null) { + location = new_location + size = new_size + } + } + } + + private class Required extends CheckBox { + val geometry = new Geometry + opaque = false + override def paintComponent(gfx: Graphics2D): Unit = { + super.paintComponent(gfx) + geometry.update(location, size) + } + } + + private object Node_Renderer_Component extends BorderPanel { + opaque = true + border = BorderFactory.createEmptyBorder(2, 2, 2, 2) + + var node_name: Document.Node.Name = Document.Node.Name.empty + + val theory_required = new Required + val document_required = new Required + + 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 + } + + 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)) + } + + val required = new BoxPanel(Orientation.Horizontal) + required.contents += theory_required + // FIXME required.contents += document_required + + layout(required) = BorderPanel.Position.West + layout(label) = BorderPanel.Position.Center + } + + private def in_required(location0: Point, p: Point, document: Boolean = false): Boolean = + Node_Renderer_Component != null && { + val required = + if (document) Node_Renderer_Component.document_required + else Node_Renderer_Component.theory_required + 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, + focused: Boolean, + name: Document.Node.Name, + index: Int + ): Component = { + val component = Node_Renderer_Component + component.node_name = name + component.theory_required.selected = theory_required.contains(name) + component.document_required.selected = document_required.contains(name) + component.label_border(name) + component.label.text = name.theory_base_name + component + } + } + + + /* GUI component */ + + val gui: ListView[Document.Node.Name] = new ListView[Document.Node.Name](Nil) { + background = { + // enforce default value + val c = UIManager.getDefaults.getColor("Panel.background") + new Color(c.getRed, c.getGreen, c.getBlue, c.getAlpha) + } + listenTo(mouse.clicks) + listenTo(mouse.moves) + reactions += { + case MouseClicked(_, point, _, clicks, _) => + val index = peer.locationToIndex(point) + if (index >= 0) { + val index_location = peer.indexToLocation(index) + val a = in_required(index_location, point) + val b = in_required(index_location, point, document = true) + if (a || b) { + if (clicks == 1) { + Document_Model.node_required(listData(index), toggle = true, document = b) + } + } + else if (clicks == 2) PIDE.editor.goto_file(true, view, listData(index).node) + } + case MouseMoved(_, point, _) => + val index = peer.locationToIndex(point) + val index_location = peer.indexToLocation(index) + if (index >= 0 && in_required(index_location, point)) { + tooltip = "Mark as required for continuous checking" + } + else if (index >= 0 && in_required(index_location, point, document = true)) { + tooltip = "Mark as required for continuous checking, with inclusion in document" + } + else if (index >= 0 && in_label(index_location, point)) { + val name = listData(index) + val st = nodes_status.overall_node_status(name) + tooltip = + "theory " + quote(name.theory) + + (if (st == Document_Status.Overall_Node_Status.ok) "" else " (" + st + ")") + } + else tooltip = null + } + } + + gui.renderer = new Node_Renderer + gui.peer.setLayoutOrientation(JList.HORIZONTAL_WRAP) + gui.peer.setVisibleRowCount(0) + gui.selection.intervalMode = ListView.IntervalMode.Single + + + /* update */ + + def update(domain: Option[Set[Document.Node.Name]] = None, trim: Boolean = false): Unit = { + GUI_Thread.require {} + + val snapshot = PIDE.session.snapshot() + + val (nodes_status_changed, nodes_status1) = + nodes_status.update( + PIDE.resources, snapshot.state, snapshot.version, domain = domain, trim = trim) + + nodes_status = nodes_status1 + if (nodes_status_changed) { + gui.listData = + (for { + (name, node_status) <- nodes_status1.present.iterator + if !node_status.is_suppressed && node_status.total > 0 + } yield name).toList + } + } + + + /* reinit */ + + def reinit(): Unit = { + GUI_Thread.require {} + + theory_required = Document_Model.required_nodes(false) + document_required = Document_Model.required_nodes(true) + gui.repaint() + } +}