# HG changeset patch
# User oheimb
# Date 917626354 -3600
# Node ID 2f354020efc350672e24e0a5bf8ee1d9bced7d9e
# Parent  a56aaad7ff2d9d96325921f26edc9f45aa5052e4
corrected output of symbols for several (probably not all) relevant functions
moved print_mode to ROOT.ML

diff -r a56aaad7ff2d -r 2f354020efc3 src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Fri Jan 29 17:12:14 1999 +0100
+++ b/src/Pure/Syntax/syntax.ML	Fri Jan 29 17:12:34 1999 +0100
@@ -353,10 +353,11 @@
     val pts = Parser.parse gram root' (Lexicon.tokenize lexicon xids chars);
 
     fun show_pt pt =
-      warning (Pretty.string_of (Ast.pretty_ast (SynTrans.pt_to_ast (K None) pt)));
+      warning (Symbol.output (Pretty.string_of 
+		(Ast.pretty_ast (SynTrans.pt_to_ast (K None) pt))));
   in
     if length pts > ! ambiguity_level then
-      (warning ("Ambiguous input " ^ quote str);
+      (warning ("Ambiguous input " ^ quote (Symbol.output str));
        warning "produces the following parse trees:";
        seq show_pt pts)
     else ();
@@ -446,13 +447,14 @@
 
 (** pretty terms, typs, sorts **)
 
+val print_mode = print_mode;
 fun pretty_t t_to_ast prt_t (syn as Syntax tabs) curried t =
   let
     val {print_trtab, print_ruletab, print_ast_trtab, tokentrtab, prtabs, ...} = tabs;
     val ast = t_to_ast (lookup_tr' print_trtab) t;
   in
     prt_t curried prtabs (lookup_tr' print_ast_trtab)
-      (lookup_tokentr tokentrtab (! Printer.print_mode))
+      (lookup_tokentr tokentrtab (! print_mode))
       (Ast.normalize_ast (lookup_ruletab print_ruletab) ast)
   end;