more thorough init;

--- a/src/Tools/jEdit/src/output_area.scala	Tue Nov 19 10:11:37 2024 +0100
+++ b/src/Tools/jEdit/src/output_area.scala	Tue Nov 19 10:14:22 2024 +0100
@@ -124,7 +124,10 @@
     }
   }
 
-  def init(): Unit = handle_update()
+  def init(): Unit = {
+    handle_update()
+    handle_resize()
+  }
 
   def exit(): Unit = delay_resize.revoke()
 }