src/Pure/Syntax/printer.ML
changeset 505 97eb677142d9
parent 504 a4f09493d929
child 506 e0ca460d6e51
equal deleted inserted replaced
504:a4f09493d929 505:97eb677142d9
   226           let val (Ts, args') = synT (symbs, args);
   226           let val (Ts, args') = synT (symbs, args);
   227           in ((if i < 0 then Pretty.fbrk else Pretty.brk i) :: Ts, args') end
   227           in ((if i < 0 then Pretty.fbrk else Pretty.brk i) :: Ts, args') end
   228       | synT (_ :: _, []) = sys_error "synT"
   228       | synT (_ :: _, []) = sys_error "synT"
   229 
   229 
   230     and parT (pr, args, p, p': int) =
   230     and parT (pr, args, p, p': int) =
   231       if p > p' orelse !show_brackets then
   231       if p > p' orelse (!show_brackets andalso p' <> max_pri) then
   232         #1 (synT ([Block (1, String "(" :: pr @ [String ")"])], args))
   232         #1 (synT ([Block (1, String "(" :: pr @ [String ")"])], args))
   233       else #1 (synT (pr, args))
   233       else #1 (synT (pr, args))
   234 
   234 
   235     and prefixT (_, a, [], _) = [Pretty.str a]
   235     and prefixT (_, a, [], _) = [Pretty.str a]
   236       | prefixT (c, _, args, p) = astT (appT (c, args), p)
   236       | prefixT (c, _, args, p) = astT (appT (c, args), p)