--- a/src/Tools/jEdit/src/document_dockable.scala Tue Dec 20 18:43:17 2022 +0100
+++ b/src/Tools/jEdit/src/document_dockable.scala Tue Dec 20 19:19:44 2022 +0100
@@ -119,9 +119,6 @@
/* document build process */
- private def document_theories(): List[Document.Node.Name] =
- PIDE.editor.document_theories()
-
private def init_state(): Unit =
current_state.change { _ => Document_Dockable.State(progress = log_progress()) }
@@ -163,7 +160,8 @@
finish_process(Nil)
GUI_Thread.later {
- theories.update(domain = Some(document_theories().toSet), trim = true)
+ val domain = PIDE.editor.document_theories().toSet
+ theories.update(domain = Some(domain), trim = true, force = true)
show_state()
show_page(theories_page)
}
@@ -290,7 +288,7 @@
}
case changed: Session.Commands_Changed =>
GUI_Thread.later {
- val domain = document_theories().filter(changed.nodes).toSet
+ val domain = PIDE.editor.document_theories().filter(changed.nodes).toSet
if (domain.nonEmpty) theories.update(domain = Some(domain))
}
}
@@ -300,7 +298,6 @@
init_state()
PIDE.session.global_options += main
PIDE.session.commands_changed += main
- theories.update(domain = Some(document_theories().toSet), force = true)
handle_resize()
delay_load.invoke()
}
--- a/src/Tools/jEdit/src/theories_status.scala Tue Dec 20 18:43:17 2022 +0100
+++ b/src/Tools/jEdit/src/theories_status.scala Tue Dec 20 19:19:44 2022 +0100
@@ -26,12 +26,10 @@
private var nodes_status = Document_Status.Nodes_Status.empty
private var nodes_required = Set.empty[Document.Node.Name]
private var document_required = Set.empty[Document.Node.Name]
- private var document_theories = List.empty[Document.Node.Name]
private def init_state(): Unit = GUI_Thread.require {
if (document) {
nodes_required = PIDE.editor.document_required().toSet
- document_theories = PIDE.editor.document_theories()
}
else {
nodes_required = Document_Model.nodes_required()
@@ -237,7 +235,9 @@
nodes_status = nodes_status1
if (nodes_status_changed || force) {
gui.listData =
- if (document) nodes_status1.present(domain = Some(document_theories)).map(_._1)
+ if (document) {
+ nodes_status1.present(domain = Some(PIDE.editor.document_theories())).map(_._1)
+ }
else {
(for {
(name, node_status) <- nodes_status1.present().iterator