simplified printer context: uniform externing and static token translations;

--- a/src/Pure/Isar/proof_context.ML	Thu Apr 07 17:38:17 2011 +0200
+++ b/src/Pure/Isar/proof_context.ML	Thu Apr 07 17:52:44 2011 +0200
@@ -400,40 +400,6 @@
   | NONE => x);
 
 
-(* default token translations *)
-
-local
-
-fun free_or_skolem ctxt x =
-  (if can Name.dest_skolem x then Pretty.mark Markup.skolem (Pretty.str (revert_skolem ctxt x))
-   else Pretty.mark Markup.free (Pretty.str x))
-  |> Pretty.mark
-    (if Variable.is_fixed ctxt x orelse Syntax.is_pretty_global ctxt then Markup.fixed x
-     else Markup.hilite);
-
-fun var_or_skolem _ s =
-  (case Lexicon.read_variable s of
-    SOME (x, i) =>
-      (case try Name.dest_skolem x of
-        NONE => Pretty.mark Markup.var (Pretty.str s)
-      | SOME x' => Pretty.mark Markup.skolem (Pretty.str (Term.string_of_vname (x', i))))
-  | NONE => Pretty.mark Markup.var (Pretty.str s));
-
-fun plain_markup m _ s = Pretty.mark m (Pretty.str s);
-
-val token_trans =
- Syntax.tokentrans_mode ""
-  [("tfree", plain_markup Markup.tfree),
-   ("tvar", plain_markup Markup.tvar),
-   ("free", free_or_skolem),
-   ("bound", plain_markup Markup.bound),
-   ("var", var_or_skolem),
-   ("numeral", plain_markup Markup.numeral),
-   ("inner_string", plain_markup Markup.inner_string)];
-
-in val _ = Context.>> (Context.map_theory (Sign.add_tokentrfuns token_trans)) end;
-
-
 
 (** prepare terms and propositions **)
 

--- a/src/Pure/Syntax/printer.ML	Thu Apr 07 17:38:17 2011 +0200
+++ b/src/Pure/Syntax/printer.ML	Thu Apr 07 17:52:44 2011 +0200
@@ -33,14 +33,15 @@
   val update_prtabs: string -> Syn_Ext.xprod list -> prtabs -> prtabs
   val remove_prtabs: string -> Syn_Ext.xprod list -> prtabs -> prtabs
   val merge_prtabs: prtabs -> prtabs -> prtabs
-  val pretty_term_ast: {extern_class: string -> xstring, extern_type: string -> xstring,
-      extern_const: string -> xstring} -> Proof.context -> bool -> prtabs ->
+  val pretty_term_ast: bool -> Proof.context -> prtabs ->
     (string -> Proof.context -> Ast.ast list -> Ast.ast) ->
-    (string -> (Proof.context -> string -> Pretty.T) option) -> Ast.ast -> Pretty.T list
-  val pretty_typ_ast: {extern_class: string -> xstring, extern_type: string -> xstring} ->
-    Proof.context -> bool -> prtabs ->
+    (string -> string -> Pretty.T option) ->
+    (string -> Markup.T list * xstring) ->
+    Ast.ast -> Pretty.T list
+  val pretty_typ_ast: Proof.context -> prtabs ->
     (string -> Proof.context -> Ast.ast list -> Ast.ast) ->
-    (string -> (Proof.context -> string -> Pretty.T) option) -> Ast.ast -> Pretty.T list
+    (string -> string -> Pretty.T option) ->
+    (string -> Markup.T list * xstring) -> Ast.ast -> Pretty.T list
 end;
 
 structure Printer: PRINTER =
@@ -166,18 +167,10 @@
 
 val pretty_priority = Config.int (Config.declare "Syntax.pretty_priority" (K (Config.Int 0)));
 
-fun pretty extern ctxt tabs trf tokentrf type_mode curried ast0 =
+fun pretty type_mode curried ctxt tabs trf token_trans markup_extern ast0 =
   let
-    val {extern_class, extern_type, extern_const} = extern;
     val show_brackets = Config.get ctxt show_brackets;
 
-    fun token_trans a x =
-      (case tokentrf a of
-        NONE =>
-          if member (op =) Syn_Ext.standard_token_classes a
-          then SOME (Pretty.str x) else NONE
-      | SOME f => SOME (f ctxt x));
-
     (*default applications: prefix / postfix*)
     val appT =
       if type_mode then Syn_Trans.tappl_ast_tr'
@@ -185,49 +178,44 @@
       else Syn_Trans.appl_ast_tr';
 
     fun synT _ ([], args) = ([], args)
-      | synT markup (Arg p :: symbs, t :: args) =
-          let val (Ts, args') = synT markup (symbs, args);
+      | synT m (Arg p :: symbs, t :: args) =
+          let val (Ts, args') = synT m (symbs, args);
           in (astT (t, p) @ Ts, args') end
-      | synT markup (TypArg p :: symbs, t :: args) =
+      | synT m (TypArg p :: symbs, t :: args) =
           let
-            val (Ts, args') = synT markup (symbs, args);
+            val (Ts, args') = synT m (symbs, args);
           in
             if type_mode then (astT (t, p) @ Ts, args')
             else
-              (pretty extern (Config.put pretty_priority p ctxt)
-                tabs trf tokentrf true curried t @ Ts, args')
+              (pretty true curried (Config.put pretty_priority p ctxt)
+                tabs trf token_trans markup_extern t @ Ts, args')
           end
-      | synT markup (String s :: symbs, args) =
-          let val (Ts, args') = synT markup (symbs, args);
-          in (markup (Pretty.str s) :: Ts, args') end
-      | synT markup (Space s :: symbs, args) =
-          let val (Ts, args') = synT markup (symbs, args);
+      | synT m (String s :: symbs, args) =
+          let val (Ts, args') = synT m (symbs, args);
+          in (Pretty.marks_str (m, s) :: Ts, args') end
+      | synT m (Space s :: symbs, args) =
+          let val (Ts, args') = synT m (symbs, args);
           in (Pretty.str s :: Ts, args') end
-      | synT markup (Block (i, bsymbs) :: symbs, args) =
+      | synT m (Block (i, bsymbs) :: symbs, args) =
           let
-            val (bTs, args') = synT markup (bsymbs, args);
-            val (Ts, args'') = synT markup (symbs, args');
+            val (bTs, args') = synT m (bsymbs, args);
+            val (Ts, args'') = synT m (symbs, args');
             val T =
               if i < 0 then Pretty.unbreakable (Pretty.block bTs)
               else Pretty.blk (i, bTs);
           in (T :: Ts, args'') end
-      | synT markup (Break i :: symbs, args) =
+      | synT m (Break i :: symbs, args) =
           let
-            val (Ts, args') = synT markup (symbs, args);
+            val (Ts, args') = synT m (symbs, args);
             val T = if i < 0 then Pretty.fbrk else Pretty.brk i;
           in (T :: Ts, args') end
 
-    and parT markup (pr, args, p, p': int) = #1 (synT markup
+    and parT m (pr, args, p, p': int) = #1 (synT m
           (if p > p' orelse (show_brackets andalso p' <> Syn_Ext.max_pri andalso not (is_chain pr))
             then [Block (1, Space "(" :: pr @ [Space ")"])]
             else pr, args))
 
-    and atomT a = a |> Lexicon.unmark
-     {case_class = fn c => Pretty.mark (Markup.tclass c) (Pretty.str (extern_class c)),
-      case_type = fn c => Pretty.mark (Markup.tycon c) (Pretty.str (extern_type c)),
-      case_const = fn c => Pretty.mark (Markup.const c) (Pretty.str (extern_const c)),
-      case_fixed = fn x => the (token_trans "_free" x),
-      case_default = Pretty.str}
+    and atomT a = Pretty.marks_str (markup_extern a)
 
     and prefixT (_, a, [], _) = [atomT a]
       | prefixT (c, _, args, p) = astT (appT (c, args), p)
@@ -239,18 +227,12 @@
     and combT (tup as (c, a, args, p)) =
       let
         val nargs = length args;
-        val markup = a |> Lexicon.unmark
-         {case_class = Pretty.mark o Markup.tclass,
-          case_type = Pretty.mark o Markup.tycon,
-          case_const = Pretty.mark o Markup.const,
-          case_fixed = Pretty.mark o Markup.fixed,
-          case_default = K I};
 
         (*find matching table entry, or print as prefix / postfix*)
         fun prnt ([], []) = prefixT tup
           | prnt ([], tb :: tbs) = prnt (Symtab.lookup_list tb a, tbs)
           | prnt ((pr, n, p') :: prnps, tbs) =
-              if nargs = n then parT markup (pr, args, p, p')
+              if nargs = n then parT (#1 (markup_extern a)) (pr, args, p, p')
               else if nargs > n andalso not type_mode then
                 astT (appT (splitT n ([c], args)), p)
               else prnt (prnps, tbs);
@@ -264,7 +246,7 @@
       | tokentrT _ _ = NONE
 
     and astT (c as Ast.Constant a, p) = combT (c, a, [], p)
-      | astT (ast as Ast.Variable x, _) = [Ast.pretty_ast ast]
+      | astT (ast as Ast.Variable _, _) = [Ast.pretty_ast ast]
       | 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)
       | astT (ast as Ast.Appl _, _) = raise Ast.AST ("pretty: malformed ast", [ast]);
@@ -273,14 +255,13 @@
 
 (* pretty_term_ast *)
 
-fun pretty_term_ast extern ctxt curried prtabs trf tokentrf ast =
-  pretty extern ctxt (mode_tabs prtabs (print_mode_value ())) trf tokentrf false curried ast;
+fun pretty_term_ast curried ctxt prtabs trf tokentrf extern ast =
+  pretty false curried ctxt (mode_tabs prtabs (print_mode_value ())) trf tokentrf extern ast;
 
 
 (* pretty_typ_ast *)
 
-fun pretty_typ_ast {extern_class, extern_type} ctxt _ prtabs trf tokentrf ast =
-  pretty {extern_class = extern_class, extern_type = extern_type, extern_const = I}
-    ctxt (mode_tabs prtabs (print_mode_value ())) trf tokentrf true false ast;
+fun pretty_typ_ast ctxt prtabs trf tokentrf extern ast =
+  pretty true false ctxt (mode_tabs prtabs (print_mode_value ())) trf tokentrf extern ast;
 
 end;

--- a/src/Pure/Syntax/syn_ext.ML	Thu Apr 07 17:38:17 2011 +0200
+++ b/src/Pure/Syntax/syn_ext.ML	Thu Apr 07 17:52:44 2011 +0200
@@ -15,11 +15,7 @@
   val mk_trfun: string * 'a -> string * ('a * stamp)
   val eq_trfun: ('a * stamp) * ('a * stamp) -> bool
   val escape: string -> string
-  val tokentrans_mode:
-    string -> (string * (Proof.context -> string -> Pretty.T)) list ->
-    (string * string * (Proof.context -> string -> Pretty.T)) list
-  val standard_token_classes: string list
-  val standard_token_markers: string list
+  val token_markers: string list
 end;
 
 signature SYN_EXT =
@@ -383,17 +379,10 @@
 fun eq_trfun ((_, s1: stamp), (_, s2)) = s1 = s2;
 
 
-(* token translations *)
-
-fun tokentrans_mode m trs = map (fn (s, f) => (m, s, f)) trs;
+(* pure_ext *)
 
-val standard_token_classes =
-  ["tfree", "tvar", "free", "bound", "var", "numeral", "inner_string"];
-
-val standard_token_markers = map (fn s => "_" ^ s) standard_token_classes;
-
-
-(* pure_ext *)
+val token_markers =
+  ["_tfree", "_tvar", "_free", "_bound", "_var", "_numeral", "_inner_string"];
 
 val pure_ext = syn_ext' false (K false)
   [Mfix ("_", spropT --> propT, "", [0], 0),
@@ -403,7 +392,7 @@
    Mfix ("'(_')", spropT --> spropT, "", [0], max_pri),
    Mfix ("_::_",  [logicT, typeT] ---> logicT, "_constrain", [4, 0], 3),
    Mfix ("_::_",  [spropT, typeT] ---> spropT, "_constrain", [4, 0], 3)]
-  standard_token_markers
+  token_markers
   ([], [], [], [])
   []
   ([], []);

--- a/src/Pure/Syntax/syntax_phases.ML	Thu Apr 07 17:38:17 2011 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Thu Apr 07 17:52:44 2011 +0200
@@ -475,7 +475,7 @@
     val {structs, fixes} = idents;
 
     fun mark_atoms ((t as Const (c, _)) $ u) =
-          if member (op =) Syntax.standard_token_markers c
+          if member (op =) Syntax.token_markers c
           then t $ u else mark_atoms t $ mark_atoms u
       | mark_atoms (t $ u) = mark_atoms t $ mark_atoms u
       | mark_atoms (Abs (x, T, t)) = Abs (x, T, mark_atoms t)
@@ -553,46 +553,66 @@
 
 local
 
-fun unparse_t t_to_ast prt_t markup ctxt curried t =
+fun free_or_skolem ctxt x =
+  let
+    val m =
+      if Variable.is_fixed ctxt x orelse Syntax.is_pretty_global ctxt
+      then Markup.fixed x
+      else Markup.hilite;
+  in
+    if can Name.dest_skolem x
+    then ([m, Markup.skolem], ProofContext.revert_skolem ctxt x)
+    else ([m, Markup.free], x)
+  end;
+
+fun var_or_skolem s =
+  (case Lexicon.read_variable s of
+    SOME (x, i) =>
+      (case try Name.dest_skolem x of
+        NONE => (Markup.var, s)
+      | SOME x' => (Markup.skolem, Term.string_of_vname (x', i)))
+  | NONE => (Markup.var, s));
+
+fun unparse_t t_to_ast prt_t markup ctxt t =
   let
     val syn = ProofContext.syn_of ctxt;
-    val tokentr = Syntax.token_translation syn (print_mode_value ());
+
+    fun token_trans "_tfree" x = SOME (Pretty.mark_str (Markup.tfree, x))
+      | token_trans "_tvar" x = SOME (Pretty.mark_str (Markup.tvar, x))
+      | token_trans "_free" x = SOME (Pretty.marks_str (free_or_skolem ctxt x))
+      | token_trans "_bound" x = SOME (Pretty.mark_str (Markup.bound, x))
+      | token_trans "_var" x = SOME (Pretty.mark_str (var_or_skolem x))
+      | token_trans "_numeral" x = SOME (Pretty.mark_str (Markup.numeral, x))
+      | token_trans "_inner_string" x = SOME (Pretty.mark_str (Markup.inner_string, x))
+      | token_trans _ _ = NONE;
+
+    val markup_extern = Lexicon.unmark
+     {case_class = fn x => ([Markup.tclass x], Type.extern_class (ProofContext.tsig_of ctxt) x),
+      case_type = fn x => ([Markup.tycon x], Type.extern_type (ProofContext.tsig_of ctxt) x),
+      case_const = fn x => ([Markup.const x], Consts.extern (ProofContext.consts_of ctxt) x),
+      case_fixed = fn x => free_or_skolem ctxt x,
+      case_default = fn x => ([], x)};
   in
     t_to_ast ctxt (Syntax.print_translation syn) t
     |> Ast.normalize ctxt (Syntax.print_rules syn)
-    |> prt_t ctxt curried (Syntax.prtabs syn) (Syntax.print_ast_translation syn) tokentr
+    |> prt_t ctxt (Syntax.prtabs syn) (Syntax.print_ast_translation syn) token_trans markup_extern
     |> Pretty.markup markup
   end;
 
 in
 
-fun unparse_sort ctxt =
-  let
-    val tsig = ProofContext.tsig_of ctxt;
-    val extern = {extern_class = Type.extern_class tsig, extern_type = I};
-  in unparse_t sort_to_ast (Printer.pretty_typ_ast extern) Markup.sort ctxt false end;
-
-fun unparse_typ ctxt =
-  let
-    val tsig = ProofContext.tsig_of ctxt;
-    val extern = {extern_class = Type.extern_class tsig, extern_type = Type.extern_type tsig};
-  in unparse_t typ_to_ast (Printer.pretty_typ_ast extern) Markup.typ ctxt false end;
+val unparse_sort = unparse_t sort_to_ast Printer.pretty_typ_ast Markup.sort;
+val unparse_typ = unparse_t typ_to_ast Printer.pretty_typ_ast Markup.typ;
 
 fun unparse_term ctxt =
   let
     val thy = ProofContext.theory_of ctxt;
     val syn = ProofContext.syn_of ctxt;
-    val tsig = ProofContext.tsig_of ctxt;
     val idents = Local_Syntax.idents_of (ProofContext.syntax_of ctxt);
-    val is_syntax_const = Syntax.is_const syn;
-    val consts = ProofContext.consts_of ctxt;
-    val extern =
-     {extern_class = Type.extern_class tsig,
-      extern_type = Type.extern_type tsig,
-      extern_const = Consts.extern consts};
   in
-    unparse_t (term_to_ast idents is_syntax_const) (Printer.pretty_term_ast extern)
-      Markup.term ctxt (not (Pure_Thy.old_appl_syntax thy))
+    unparse_t (term_to_ast idents (Syntax.is_const syn))
+      (Printer.pretty_term_ast (not (Pure_Thy.old_appl_syntax thy)))
+      Markup.term ctxt
   end;
 
 end;