# HG changeset patch
# User nipkow
# Date 775811230 -7200
# Node ID a4f09493d929ef919e4896bbb9c823382e3a8956
# Parent  15375d7b379c52015a9d9d86a0f15df2f8e49a3f
added flag show_brackets for printinmg fully bracketed terms.

diff -r 15375d7b379c -r a4f09493d929 src/Pure/Syntax/printer.ML
--- a/src/Pure/Syntax/printer.ML	Mon Aug 01 17:34:57 1994 +0200
+++ b/src/Pure/Syntax/printer.ML	Tue Aug 02 09:07:10 1994 +0200
@@ -7,8 +7,9 @@
 
 signature PRINTER0 =
 sig
+  val show_brackets: bool ref
+  val show_sorts: bool ref
   val show_types: bool ref
-  val show_sorts: bool ref
 end;
 
 signature PRINTER =
@@ -44,7 +45,7 @@
 
 val show_types = ref false;
 val show_sorts = ref false;
-
+val show_brackets = ref false;
 
 
 (** convert term or typ to ast **)
@@ -227,7 +228,7 @@
       | synT (_ :: _, []) = sys_error "synT"
 
     and parT (pr, args, p, p': int) =
-      if p > p' then
+      if p > p' orelse !show_brackets then
         #1 (synT ([Block (1, String "(" :: pr @ [String ")"])], args))
       else #1 (synT (pr, args))