# HG changeset patch
# User wenzelm
# Date 1670495083 -3600
# Node ID 9f97eda3fcf1204421010ff6d4db975f1536966c
# Parent  faea52979f547eda92f50cc8e19b018436a70cc5
tuned;

diff -r faea52979f54 -r 9f97eda3fcf1 src/Tools/jEdit/src/theories_status.scala
--- a/src/Tools/jEdit/src/theories_status.scala	Thu Dec 08 11:16:35 2022 +0100
+++ b/src/Tools/jEdit/src/theories_status.scala	Thu Dec 08 11:24:43 2022 +0100
@@ -168,6 +168,7 @@
   /* GUI component */
 
   val gui: ListView[Document.Node.Name] = new ListView[Document.Node.Name](Nil) {
+    renderer = new Node_Renderer
     background = {
       // enforce default value
       val c = UIManager.getDefaults.getColor("Panel.background")
@@ -207,13 +208,12 @@
         }
         else tooltip = null
     }
+
+    peer.setLayoutOrientation(JList.HORIZONTAL_WRAP)
+    peer.setVisibleRowCount(0)
+    selection.intervalMode = ListView.IntervalMode.Single
   }
 
-  gui.renderer = new Node_Renderer
-  gui.peer.setLayoutOrientation(JList.HORIZONTAL_WRAP)
-  gui.peer.setVisibleRowCount(0)
-  gui.selection.intervalMode = ListView.IntervalMode.Single
-
 
   /* update */