--- a/src/Tools/jEdit/src/simplifier_trace_dockable.scala Thu Nov 07 12:35:55 2024 +0100
+++ b/src/Tools/jEdit/src/simplifier_trace_dockable.scala Thu Nov 07 13:22:59 2024 +0100
@@ -61,11 +61,7 @@
new Simplifier_Trace_Window(view, current_snapshot, trace)
}
- private def handle_resize(): Unit = {
- GUI_Thread.later {
- text_area.resize(Font_Info.main(scale = PIDE.options.real("jedit_font_scale")))
- }
- }
+ private def handle_resize(): Unit = text_area.zoom()
private def handle_update(follow: Boolean): Unit = {
val (new_snapshot, new_command, new_results, new_id) =