1.1 --- a/src/Pure/Syntax/printer.ML	Sat May 29 15:07:05 2004 +0200
     1.2 +++ b/src/Pure/Syntax/printer.ML	Sat May 29 15:07:29 2004 +0200
     1.3 @@ -13,6 +13,7 @@
     1.4    val show_types: bool ref
     1.5    val show_no_free_types: bool ref
     1.6    val show_all_types: bool ref
     1.7 +  val pp_show_brackets: Pretty.pp -> Pretty.pp
     1.8  end;
     1.9  
    1.10  signature PRINTER =
    1.11 @@ -45,6 +46,10 @@
    1.12  val show_no_free_types = ref false;
    1.13  val show_all_types = ref false;
    1.14  
    1.15 +fun pp_show_brackets pp = Pretty.pp (setmp show_brackets true (Pretty.term pp))
    1.16 +  (Pretty.typ pp) (Pretty.sort pp) (Pretty.classrel pp) (Pretty.arity pp);
    1.17 +
    1.18 +
    1.19  
    1.20  (** misc utils **)
    1.21  
    1.22 @@ -293,10 +298,15 @@
    1.23            let
    1.24              val (bTs, args') = synT (bsymbs, args);
    1.25              val (Ts, args'') = synT (symbs, args');
    1.26 -          in (Pretty.blk (i, bTs) :: Ts, args'') end
    1.27 +            val T =
    1.28 +              if i < 0 then Pretty.unbreakable (Pretty.block bTs)
    1.29 +              else Pretty.blk (i, bTs);
    1.30 +          in (T :: Ts, args'') end
    1.31        | synT (Break i :: symbs, args) =
    1.32 -          let val (Ts, args') = synT (symbs, args);
    1.33 -          in ((if i < 0 then Pretty.fbrk else Pretty.brk i) :: Ts, args') end
    1.34 +          let
    1.35 +            val (Ts, args') = synT (symbs, args);
    1.36 +            val T = if i < 0 then Pretty.fbrk else Pretty.brk i;
    1.37 +          in (T :: Ts, args') end
    1.38        | synT (_ :: _, []) = sys_error "synT"
    1.39  
    1.40      and parT (pr, args, p, p': int) = #1 (synT