clarified module initialization;
authorwenzelm
Mon, 19 Dec 2022 14:39:22 +0100
changeset 76713 d8b3b8a179c2
parent 76712 63c0a456b977
child 76714 95a926d483c5
clarified module initialization;
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()
 }