# HG changeset patch # User wenzelm # Date 1671560384 -3600 # Node ID 2c8632c746fe019224f7436b1a3e764eb82d6e9e # Parent 3f50b24909dfae4726d2f77fed911aae5f14b471 proper handling of state updates; diff -r 3f50b24909df -r 2c8632c746fe src/Tools/jEdit/src/document_dockable.scala --- 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() } diff -r 3f50b24909df -r 2c8632c746fe src/Tools/jEdit/src/theories_status.scala --- 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