# HG changeset patch
# User wenzelm
# Date 1734530011 -3600
# Node ID 79079d94095b392820584f0ef933904a3be8bb6c
# Parent  e5be995d21f0846a084a99b24de1bdf11b112621
tuned output: suppress vacuous nodes from 07ad0b407d38;

diff -r e5be995d21f0 -r 79079d94095b src/Pure/Syntax/parser.ML
--- 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 [];