--- 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("<html><b>Build</b></html>") {
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 = {
--- 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)