# HG changeset patch
# User wenzelm
# Date 1730991833 -3600
# Node ID 365b9aac4363c129aa692226b3cdb5a6f0efd5ee
# Parent  71e66ebbc6323bb35d39b23ec95823a5487b93a1
tuned;

diff -r 71e66ebbc632 -r 365b9aac4363 src/Tools/jEdit/src/simplifier_trace_window.scala
--- a/src/Tools/jEdit/src/simplifier_trace_window.scala	Thu Nov 07 15:42:35 2024 +0100
+++ b/src/Tools/jEdit/src/simplifier_trace_window.scala	Thu Nov 07 16:03:53 2024 +0100
@@ -150,8 +150,8 @@
   handle_resize()
 
   def handle_update(): Unit = {
-    val xml = Pretty.separate(tree.tree_children.flatMap(_.format))
-    pretty_text_area.update(snapshot, Command.Results.empty, xml)
+    val output = tree.tree_children.flatMap(_.format)
+    pretty_text_area.update(snapshot, Command.Results.empty, Pretty.separate(output))
   }
 
   def handle_resize(): Unit = pretty_text_area.zoom()