--- 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 */