# HG changeset patch
# User wenzelm
# Date 1085836049 -7200
# Node ID 827c68f8267ca83e514958f2f6293d1834dc7187
# Parent  ba0fc27a6c7ed6c67d692c69eae9b99bc08b2421
added pp_show_brackets; support unbreakable blocks;

diff -r ba0fc27a6c7e -r 827c68f8267c src/Pure/Syntax/printer.ML
--- a/src/Pure/Syntax/printer.ML	Sat May 29 15:07:05 2004 +0200
+++ b/src/Pure/Syntax/printer.ML	Sat May 29 15:07:29 2004 +0200
@@ -13,6 +13,7 @@
   val show_types: bool ref
   val show_no_free_types: bool ref
   val show_all_types: bool ref
+  val pp_show_brackets: Pretty.pp -> Pretty.pp
 end;
 
 signature PRINTER =
@@ -45,6 +46,10 @@
 val show_no_free_types = ref false;
 val show_all_types = ref false;
 
+fun pp_show_brackets pp = Pretty.pp (setmp show_brackets true (Pretty.term pp))
+  (Pretty.typ pp) (Pretty.sort pp) (Pretty.classrel pp) (Pretty.arity pp);
+
+
 
 (** misc utils **)
 
@@ -293,10 +298,15 @@
           let
             val (bTs, args') = synT (bsymbs, args);
             val (Ts, args'') = synT (symbs, args');
-          in (Pretty.blk (i, bTs) :: Ts, args'') end
+            val T =
+              if i < 0 then Pretty.unbreakable (Pretty.block bTs)
+              else Pretty.blk (i, bTs);
+          in (T :: Ts, args'') end
       | synT (Break i :: symbs, args) =
-          let val (Ts, args') = synT (symbs, args);
-          in ((if i < 0 then Pretty.fbrk else Pretty.brk i) :: Ts, args') end
+          let
+            val (Ts, args') = synT (symbs, args);
+            val T = if i < 0 then Pretty.fbrk else Pretty.brk i;
+          in (T :: Ts, args') end
       | synT (_ :: _, []) = sys_error "synT"
 
     and parT (pr, args, p, p': int) = #1 (synT