# HG changeset patch
# User wenzelm
# Date 918764230 -3600
# Node ID 94ce639eb7e58d6023a6405ce072e78bf2b53b47
# Parent  52d99d68d3befb3d9685a1339c0b4babb78b00ee
proper handling of print_mode wrt. Pretty.sym;

diff -r 52d99d68d3be -r 94ce639eb7e5 src/Pure/Syntax/printer.ML
--- a/src/Pure/Syntax/printer.ML	Thu Feb 11 21:16:30 1999 +0100
+++ b/src/Pure/Syntax/printer.ML	Thu Feb 11 21:17:10 1999 +0100
@@ -201,11 +201,11 @@
           (if Lexicon.is_terminal s then SynExt.max_pri else p);
 
         fun xsyms_to_syms (SynExt.Delim s :: xsyms) =
-              apfst (cons_str (Symbol.output s)) (xsyms_to_syms xsyms)
+              apfst (cons_str s) (xsyms_to_syms xsyms)
           | xsyms_to_syms (SynExt.Argument s_p :: xsyms) =
               apfst (cons (arg s_p)) (xsyms_to_syms xsyms)
           | xsyms_to_syms (SynExt.Space s :: xsyms) =
-              apfst (cons_str (Symbol.output s)) (xsyms_to_syms xsyms)
+              apfst (cons_str s) (xsyms_to_syms xsyms)
           | xsyms_to_syms (SynExt.Bg i :: xsyms) =
               let
                 val (bsyms, xsyms') = xsyms_to_syms xsyms;
@@ -292,7 +292,7 @@
           end
       | synT (String s :: symbs, args) =
           let val (Ts, args') = synT (symbs, args);
-          in (Pretty.str s :: Ts, args') end
+          in (Pretty.sym s :: Ts, args') end
       | synT (Block (i, bsymbs) :: symbs, args) =
           let
             val (bTs, args') = synT (bsymbs, args);
@@ -309,7 +309,7 @@
             then [Block (1, String "(" :: pr @ [String ")"])]
             else pr, args))
 
-    and prefixT (_, a, [], _) = [Pretty.str a]
+    and prefixT (_, a, [], _) = [Pretty.sym a]
       | prefixT (c, _, args, p) =
           if c = Ast.Constant "_appl" orelse c = Ast.Constant "_applC" then
             error "Syntax insufficient for printing prefix applications!"
@@ -333,13 +333,13 @@
               else prnt prnps;
       in
         (case token_trans a args of     (*try token translation function*)
-          Some (s, len) => [Pretty.strlen s len]
+          Some (s, len) => [Pretty.strlen s len]	(* FIXME Pretty.sym (!?) *)
         | None =>			(*try print translation functions*)
             astT (trans a (trf a) args, p) handle Match => prnt (get_fmts tabs a))
       end
 
     and astT (c as Ast.Constant a, p) = combT (c, a, [], p)
-      | astT (Ast.Variable x, _) = [Pretty.str x]
+      | astT (Ast.Variable x, _) = [Pretty.sym x]
       | astT (Ast.Appl ((c as Ast.Constant a) :: (args as _ :: _)), p) =
           combT (c, a, args, p)
       | astT (Ast.Appl (f :: (args as _ :: _)), p) = astT (appT (f, args), p)