proper handling of state updates;
authorwenzelm
Tue, 20 Dec 2022 19:19:44 +0100
changeset 76719 2c8632c746fe
parent 76718 3f50b24909df
child 76720 37f7b2965e02
proper handling of state updates;
src/Tools/jEdit/src/document_dockable.scala
src/Tools/jEdit/src/theories_status.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()
   }
--- 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