added flag show_brackets for printinmg fully bracketed terms.
--- 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))