tuned;

--- a/src/Tools/jEdit/src/pretty_text_area.scala	Thu Nov 07 12:17:18 2024 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Thu Nov 07 12:26:36 2024 +0100
@@ -115,9 +115,7 @@
     }
   }
 
-  def resize(font_info: Font_Info): Unit = {
-    GUI_Thread.require {}
-
+  def resize(font_info: Font_Info): Unit = GUI_Thread.require {
     current_font_info = font_info
     refresh()
   }