tuned;

--- a/src/Tools/jEdit/src/session_build.scala	Fri Nov 24 16:17:29 2023 +0100
+++ b/src/Tools/jEdit/src/session_build.scala	Fri Nov 24 18:23:45 2023 +0100
@@ -40,11 +40,10 @@
 
     /* text */
 
-    private val text = new TextArea {
-      editable = false
-      columns = 60
-      rows = 24
-    }
+    private val text = new TextArea
+    text.editable = false
+    text.columns = 60
+    text.rows = 24
     text.font = GUI.copy_font((new Label).font)
 
     private val scroll_text = new ScrollPane(text)