# HG changeset patch
# User wenzelm
# Date 1144529493 -7200
# Node ID ae4a225e0c1fd016e2a7a5ff13d6b5513f1e4339
# Parent  f2446ce045901cdee43beddd97e4db1fb4ed3b38
pretty: late externing of consts (support authentic syntax);

diff -r f2446ce04590 -r ae4a225e0c1f src/Pure/Syntax/printer.ML
--- a/src/Pure/Syntax/printer.ML	Sat Apr 08 22:51:31 2006 +0200
+++ b/src/Pure/Syntax/printer.ML	Sat Apr 08 22:51:33 2006 +0200
@@ -29,7 +29,7 @@
   val extend_prtabs: string -> SynExt.xprod list -> prtabs -> prtabs
   val remove_prtabs: string -> SynExt.xprod list -> prtabs -> prtabs
   val merge_prtabs: prtabs -> prtabs -> prtabs
-  val pretty_term_ast: Context.generic -> bool -> prtabs
+  val pretty_term_ast: (string -> xstring) -> Context.generic -> bool -> prtabs
     -> (string -> (Context.generic -> Ast.ast list -> Ast.ast) list)
     -> (string -> (string -> string * real) option) -> Ast.ast -> Pretty.T
   val pretty_typ_ast: Context.generic -> bool -> prtabs
@@ -265,7 +265,7 @@
   | is_chain [Arg _] = true
   | is_chain _  = false;
 
-fun pretty context tabs trf tokentrf type_mode curried ast0 p0 =
+fun pretty extern_const context tabs trf tokentrf type_mode curried ast0 p0 =
   let
     val trans = apply_trans context "print ast translation";
 
@@ -290,7 +290,7 @@
             val (Ts, args') = synT (symbs, args);
           in
             if type_mode then (astT (t, p) @ Ts, args')
-            else (pretty context tabs trf tokentrf true curried t p @ Ts, args')
+            else (pretty I context tabs trf tokentrf true curried t p @ Ts, args')
           end
       | synT (String s :: symbs, args) =
           let val (Ts, args') = synT (symbs, args);
@@ -316,7 +316,18 @@
             then [Block (1, String "(" :: pr @ [String ")"])]
             else pr, args))
 
-    and prefixT (_, a, [], _) = [Pretty.str a]
+    and atomT a =
+      (case try (unprefix Lexicon.constN) a of
+        SOME c => Pretty.str (extern_const c)
+      | NONE =>
+          (case try (unprefix Lexicon.fixedN) a of
+            SOME x =>
+              (case tokentrf "_free" of
+                SOME f => Pretty.raw_str (f x)
+              | NONE => Pretty.str x)
+          | NONE => Pretty.str a))
+
+    and prefixT (_, a, [], _) = [atomT a]
       | prefixT (c, _, args, p) = astT (appT (c, args), p)
 
     and splitT 0 ([x], ys) = (x, ys)
@@ -338,7 +349,7 @@
               else prnt (prnps, tbs);
       in
         (case token_trans a args of     (*try token translation function*)
-          SOME s_len => [Pretty.raw_str s_len]
+          SOME s => [Pretty.raw_str s]
         | NONE =>                       (*try print translation functions*)
             astT (trans a (trf a) args, p) handle Match => prnt ([], tabs))
       end
@@ -353,15 +364,15 @@
 
 (* pretty_term_ast *)
 
-fun pretty_term_ast context curried prtabs trf tokentrf ast =
-  Pretty.blk (0, pretty context (mode_tabs prtabs (! print_mode))
+fun pretty_term_ast extern_const context curried prtabs trf tokentrf ast =
+  Pretty.blk (0, pretty extern_const context (mode_tabs prtabs (! print_mode))
     trf tokentrf false curried ast 0);
 
 
 (* pretty_typ_ast *)
 
 fun pretty_typ_ast context _ prtabs trf tokentrf ast =
-  Pretty.blk (0, pretty context (mode_tabs prtabs (! print_mode))
+  Pretty.blk (0, pretty I context (mode_tabs prtabs (! print_mode))
     trf tokentrf true false ast 0);
 
 end;