initial update of nodes_required, for proper GUI state;
authorwenzelm
Mon, 05 Aug 2013 11:08:54 +0200
changeset 52860 f155c38242c1
parent 52859 f31624cc4467
child 52861 e93d73b51fd0
initial update of nodes_required, for proper GUI state;
src/Tools/jEdit/src/theories_dockable.scala
--- a/src/Tools/jEdit/src/theories_dockable.scala	Mon Aug 05 11:01:17 2013 +0200
+++ b/src/Tools/jEdit/src/theories_dockable.scala	Mon Aug 05 11:08:54 2013 +0200
@@ -100,6 +100,7 @@
       if model.node_required
     } nodes_required += model.name
   }
+  update_nodes_required()
 
   private def in_checkbox(loc0: Point, p: Point): Boolean =
     Node_Renderer_Component != null &&