# HG changeset patch # User wenzelm # Date 1670504579 -3600 # Node ID b5dfe15516375545822bb84be463723e86615d71 # Parent 01978b4acdafb9d88087697b50629fa8df38f27a more specific GUI for document nodes; diff -r 01978b4acdaf -r b5dfe1551637 src/Tools/jEdit/src/document_dockable.scala --- a/src/Tools/jEdit/src/document_dockable.scala Thu Dec 08 11:55:35 2022 +0100 +++ b/src/Tools/jEdit/src/document_dockable.scala Thu Dec 08 14:02:59 2022 +0100 @@ -13,6 +13,7 @@ import java.awt.event.{ComponentEvent, ComponentAdapter} import scala.swing.{ScrollPane, TextArea, Label, TabbedPane, BorderPanel, Component} +import scala.swing.event.SelectionChanged import org.gjt.sp.jedit.{jEdit, View} @@ -191,9 +192,17 @@ /* controls */ + private lazy val delay_load: Delay = + Delay.last(PIDE.options.seconds("editor_load_delay"), gui = true) { + val models = Document_Model.get_models() + val thy_files = PIDE.resources.resolve_dependencies(models, Nil) + } + private val document_session = JEdit_Sessions.document_selector(PIDE.options, standalone = true) + document_session.reactions += { case SelectionChanged(_) => delay_load.invoke() } + private val build_button = new GUI.Button("Build") { tooltip = "Build document" @@ -223,7 +232,7 @@ /* message pane with pages */ - private val theories = new Theories_Status(view) + private val theories = new Theories_Status(view, document = true) private val theories_page = new TabbedPane.Page("Theories", new BorderPanel { @@ -271,6 +280,7 @@ PIDE.session.commands_changed += main theories.update() handle_resize() + delay_load.invoke() } override def exit(): Unit = { diff -r 01978b4acdaf -r b5dfe1551637 src/Tools/jEdit/src/theories_status.scala --- a/src/Tools/jEdit/src/theories_status.scala Thu Dec 08 11:55:35 2022 +0100 +++ b/src/Tools/jEdit/src/theories_status.scala Thu Dec 08 14:02:59 2022 +0100 @@ -20,7 +20,7 @@ import org.gjt.sp.jedit.View -class Theories_Status(view: View) { +class Theories_Status(view: View, document: Boolean = false) { /* component state -- owned by GUI thread */ private var nodes_status = Document_Status.Nodes_Status.empty @@ -50,23 +50,20 @@ } } - 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 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 { @@ -127,21 +124,12 @@ 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_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) @@ -156,8 +144,8 @@ ): 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.required.selected = + (if (document) document_required else theory_required).contains(name) component.label_border(name) component.label.text = name.theory_base_name component @@ -181,11 +169,9 @@ 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 (in_required(index_location, point)) { if (clicks == 1) { - Document_Model.node_required(listData(index), toggle = true, document = b) + Document_Model.node_required(listData(index), toggle = true, document = document) } } else if (clicks == 2) PIDE.editor.goto_file(true, view, listData(index).node) @@ -194,10 +180,9 @@ 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" + tooltip = + if (document) "Mark for inclusion in document" + else "Mark as required for continuous checking" } else if (index >= 0 && in_label(index_location, point)) { val name = listData(index)