# HG changeset patch
# User nipkow
# Date 775899942 -7200
# Node ID e0ca460d6e518f241a31f12bad6280e5c07dee10
# Parent  97eb677142d943f37b94b6b131ea78a6b4917d7a
improved show_brackets again - Trueprop does not create () any more.

diff -r 97eb677142d9 -r e0ca460d6e51 src/Pure/Syntax/printer.ML
--- a/src/Pure/Syntax/printer.ML	Tue Aug 02 20:08:57 1994 +0200
+++ b/src/Pure/Syntax/printer.ML	Wed Aug 03 09:45:42 1994 +0200
@@ -142,7 +142,7 @@
 
         fun arg (s, p) =
           (if s = "type" then TypArg else Arg)
-          (if is_terminal s then 1000 else p);
+          (if is_terminal s then max_pri else p);
 
         fun xsyms_to_syms (Delim s :: xsyms) =
               apfst (cons_str s) (xsyms_to_syms xsyms)
@@ -197,6 +197,10 @@
 
 (** pretty term or typ asts **)
 
+fun chain[Block(_,pr)] = chain(pr)
+  | chain[Arg _] = true
+  | chain _  = false;
+
 fun pretty prtab trf type_mode ast0 p0 =
   let
     val trans = apply_trans "print ast translation";
@@ -228,9 +232,12 @@
       | synT (_ :: _, []) = sys_error "synT"
 
     and parT (pr, args, p, p': int) =
-      if p > p' orelse (!show_brackets andalso p' <> max_pri) then
-        #1 (synT ([Block (1, String "(" :: pr @ [String ")"])], args))
-      else #1 (synT (pr, args))
+          #1 (synT(if p > p' orelse
+                      (!show_brackets andalso p' <> max_pri andalso
+                       not(chain pr))
+                   then [Block (1, String "(" :: pr @ [String ")"])]
+                   else pr,
+                   args))
 
     and prefixT (_, a, [], _) = [Pretty.str a]
       | prefixT (c, _, args, p) = astT (appT (c, args), p)