more abstract syntax translation;

--- a/src/Pure/Syntax/syntax.ML	Wed Apr 06 15:43:45 2011 +0200
+++ b/src/Pure/Syntax/syntax.ML	Wed Apr 06 16:15:57 2011 +0200
@@ -118,6 +118,12 @@
   val is_keyword: syntax -> string -> bool
   val tokenize: syntax -> bool -> Symbol_Pos.T list -> Lexicon.token list
   val parse: Proof.context -> syntax -> string -> Lexicon.token list -> Parser.parsetree list
+  val parse_ast_translation: syntax -> string -> (Proof.context -> Ast.ast list -> Ast.ast) option
+  val parse_translation: syntax -> string -> (Proof.context -> term list -> term) option
+  val print_translation: syntax -> string -> (Proof.context -> typ -> term list -> term) list
+  val print_ast_translation: syntax -> string -> (Proof.context -> Ast.ast list -> Ast.ast) list
+  val token_translation: syntax -> string list ->
+    string -> (Proof.context -> string -> Pretty.T) option
   type mode
   val mode_default: mode
   val mode_input: mode
@@ -402,6 +408,8 @@
 fun err_dup_trfun name c =
   error ("More than one " ^ name ^ " for " ^ quote c);
 
+fun lookup_tr tab c = Option.map fst (Symtab.lookup tab c);
+
 fun remove_trtab trfuns = fold (Symtab.remove Syn_Ext.eq_trfun) trfuns;
 
 fun update_trtab name trfuns tab = fold Symtab.update_new trfuns (remove_trtab trfuns tab)
@@ -413,6 +421,8 @@
 
 (* print (ast) translations *)
 
+fun lookup_tr' tab c = map fst (Symtab.lookup_list tab c);
+
 fun update_tr'tab trfuns = fold_rev (Symtab.update_list Syn_Ext.eq_trfun) trfuns;
 fun remove_tr'tab trfuns = fold (Symtab.remove_list Syn_Ext.eq_trfun) trfuns;
 fun merge_tr'tabs tab1 tab2 = Symtab.merge_list Syn_Ext.eq_trfun (tab1, tab2);
@@ -495,6 +505,12 @@
 fun tokenize (Syntax ({lexicon, ...}, _)) = Lexicon.tokenize lexicon;
 fun parse ctxt (Syntax ({gram, ...}, _)) = Parser.parse ctxt gram;
 
+fun parse_ast_translation (Syntax ({parse_ast_trtab, ...}, _)) = lookup_tr parse_ast_trtab;
+fun parse_translation (Syntax ({parse_trtab, ...}, _)) = lookup_tr parse_trtab;
+fun print_translation (Syntax ({print_trtab, ...}, _)) = lookup_tr' print_trtab;
+fun print_ast_translation (Syntax ({print_ast_trtab, ...}, _)) = lookup_tr' print_ast_trtab;
+fun token_translation (Syntax ({tokentrtab, ...}, _)) = lookup_tokentr tokentrtab;
+
 type mode = string * bool;
 val mode_default = ("", true);
 val mode_input = (Print_Mode.input, true);

--- a/src/Pure/Syntax/syntax_phases.ML	Wed Apr 06 15:43:45 2011 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Wed Apr 06 16:15:57 2011 +0200
@@ -89,8 +89,6 @@
 
 (* parsetree_to_ast *)
 
-fun lookup_tr tab c = Option.map fst (Symtab.lookup tab c);
-
 fun parsetree_to_ast ctxt constrain_pos trf parsetree =
   let
     val tsig = ProofContext.tsig_of ctxt;
@@ -240,7 +238,7 @@
 fun parse_asts ctxt raw root (syms, pos) =
   let
     val syn = ProofContext.syn_of ctxt;
-    val {parse_ast_trtab, ...} = Syntax.rep_syntax syn;
+    val ast_tr = Syntax.parse_ast_translation syn;
 
     val toks = Syntax.tokenize syn raw syms;
     val _ = List.app (Lexicon.report_token ctxt) toks;
@@ -263,14 +261,16 @@
             map (Pretty.string_of o Parser.pretty_parsetree) (take limit pts))));
 
     val constrain_pos = not raw andalso Config.get ctxt Syntax.positions;
-    val parsetree_to_ast = parsetree_to_ast ctxt constrain_pos (lookup_tr parse_ast_trtab);
+    val parsetree_to_ast = parsetree_to_ast ctxt constrain_pos ast_tr;
   in map parsetree_to_ast pts end;
 
 fun parse_raw ctxt root input =
   let
-    val {parse_ruletab, parse_trtab, ...} = Syntax.rep_syntax (ProofContext.syn_of ctxt);
+    val syn = ProofContext.syn_of ctxt;
+    val tr = Syntax.parse_translation syn;
+    val {parse_ruletab, ...} = Syntax.rep_syntax syn;
     val norm = Ast.normalize ctxt (Symtab.lookup_list parse_ruletab);
-    val ast_to_term = ast_to_term ctxt (lookup_tr parse_trtab);
+    val ast_to_term = ast_to_term ctxt tr;
   in
     parse_asts ctxt false root input
     |> (map o apsnd o Exn.maps_result) (norm #> Exn.interruptible_capture ast_to_term)
@@ -558,17 +558,18 @@
 
 local
 
-fun lookup_tr' tab c = map fst (Symtab.lookup_list tab c);
-
 fun unparse_t t_to_ast prt_t markup ctxt curried t =
   let
-    val {print_trtab, print_ruletab, print_ast_trtab, tokentrtab, prtabs, ...} =
-      Syntax.rep_syntax (ProofContext.syn_of ctxt);
-    val ast = t_to_ast ctxt (lookup_tr' print_trtab) t;
+    val syn = ProofContext.syn_of ctxt;
+    val tr' = Syntax.print_translation syn;
+    val ast_tr' = Syntax.print_ast_translation syn;
+    val tokentr = Syntax.token_translation syn (print_mode_value ());
+    val {print_ruletab, tokentrtab, prtabs, ...} = Syntax.rep_syntax syn;
   in
-    Pretty.markup markup (prt_t ctxt curried prtabs (lookup_tr' print_ast_trtab)
-      (Syntax.lookup_tokentr tokentrtab (print_mode_value ()))
-      (Ast.normalize ctxt (Symtab.lookup_list print_ruletab) ast))
+    t_to_ast ctxt tr' t
+    |> Ast.normalize ctxt (Symtab.lookup_list print_ruletab)
+    |> prt_t ctxt curried prtabs ast_tr' tokentr
+    |> Pretty.markup markup
   end;
 
 in