tuned output: suppress vacuous nodes from 07ad0b407d38;

--- a/src/Pure/Syntax/parser.ML	Wed Dec 18 13:49:55 2024 +0100
+++ b/src/Pure/Syntax/parser.ML	Wed Dec 18 14:53:31 2024 +0100
@@ -544,7 +544,10 @@
 
 fun pretty_tree (Markup (_, ts)) = maps pretty_tree ts
   | pretty_tree (Node ({const = c, ...}, ts)) =
-      [Pretty.enclose "(" ")" (Pretty.breaks (Pretty.quote (Pretty.str c) :: maps pretty_tree ts))]
+      let val body = maps pretty_tree ts in
+        if c = "" then body
+        else [Pretty.enclose "(" ")" (Pretty.breaks (Pretty.quote (Pretty.str c) :: body))]
+      end
   | pretty_tree (Tip tok) =
       if Lexicon.valued_token tok then [Pretty.str (Lexicon.str_of_token tok)] else [];