# HG changeset patch
# User wenzelm
# Date 1671457162 -3600
# Node ID d8b3b8a179c250eaba0412cb51416cfb16635b63
# Parent  63c0a456b977d681105ff97b2f9ccb6064fbd851
clarified module initialization;

diff -r 63c0a456b977 -r d8b3b8a179c2 src/Tools/jEdit/src/theories_status.scala
--- a/src/Tools/jEdit/src/theories_status.scala	Mon Dec 19 14:27:26 2022 +0100
+++ b/src/Tools/jEdit/src/theories_status.scala	Mon Dec 19 14:39:22 2022 +0100
@@ -24,8 +24,13 @@
   /* component state -- owned by GUI thread */
 
   private var nodes_status = Document_Status.Nodes_Status.empty
-  private var theory_required: Set[Document.Node.Name] = Document_Model.required_nodes(false)
-  private var document_required: Set[Document.Node.Name] = Document_Model.required_nodes(true)
+  private var theory_required = Set.empty[Document.Node.Name]
+  private var document_required = Set.empty[Document.Node.Name]
+
+  private def init_state(): Unit = GUI_Thread.require {
+    theory_required = Document_Model.required_nodes(false)
+    document_required = Document_Model.required_nodes(true)
+  }
 
 
   /* node renderer */
@@ -231,11 +236,10 @@
 
   /* refresh */
 
-  def refresh(): Unit = {
-    GUI_Thread.require {}
-
-    theory_required = Document_Model.required_nodes(false)
-    document_required = Document_Model.required_nodes(true)
+  def refresh(): Unit = GUI_Thread.require {
+    init_state()
     gui.repaint()
   }
+
+  init_state()
 }