# HG changeset patch
# User wenzelm
# Date 1302102906 -7200
# Node ID 097c93dcd87727f8a72605d8f7cf875fc348a044
# Parent  f427c9890c46596e08d72f3349689187ba63bb03
eliminated slightly odd Syntax.rep_syntax;

diff -r f427c9890c46 -r 097c93dcd877 src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Wed Apr 06 17:00:40 2011 +0200
+++ b/src/Pure/Syntax/syntax.ML	Wed Apr 06 17:15:06 2011 +0200
@@ -100,32 +100,21 @@
       string list -> string -> (Proof.context -> string -> Pretty.T) option
   type ruletab
   type syntax
-  val rep_syntax: syntax ->
-   {input: Syn_Ext.xprod list,
-    lexicon: Scan.lexicon,
-    gram: Parser.gram,
-    consts: string list,
-    prmodes: string list,
-    parse_ast_trtab: ((Proof.context -> Ast.ast list -> Ast.ast) * stamp) Symtab.table,
-    parse_ruletab: ruletab,
-    parse_trtab: ((Proof.context -> term list -> term) * stamp) Symtab.table,
-    print_trtab: ((Proof.context -> typ -> term list -> term) * stamp) list Symtab.table,
-    print_ruletab: ruletab,
-    print_ast_trtab: ((Proof.context -> Ast.ast list -> Ast.ast) * stamp) list Symtab.table,
-    tokentrtab: (string * (string * ((Proof.context -> string -> Pretty.T) * stamp)) list) list,
-    prtabs: Printer.prtabs}
   val eq_syntax: syntax * syntax -> bool
   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_rules: syntax -> string -> (Ast.ast * Ast.ast) list
   val parse_translation: syntax -> string -> (Proof.context -> term list -> term) option
   val print_translation: syntax -> string ->
     Proof.context -> typ -> term list -> term  (*exception Match*)
+  val print_rules: syntax -> string -> (Ast.ast * Ast.ast) list
   val print_ast_translation: syntax -> string ->
     Proof.context -> Ast.ast list -> Ast.ast  (*exception Match*)
   val token_translation: syntax -> string list ->
     string -> (Proof.context -> string -> Pretty.T) option
+  val prtabs: syntax -> Printer.prtabs
   type mode
   val mode_default: mode
   val mode_input: mode
@@ -521,10 +510,14 @@
 
 fun parse_ast_translation (Syntax ({parse_ast_trtab, ...}, _)) = lookup_tr parse_ast_trtab;
 fun parse_translation (Syntax ({parse_trtab, ...}, _)) = lookup_tr parse_trtab;
+fun parse_rules (Syntax ({parse_ruletab, ...}, _)) = Symtab.lookup_list parse_ruletab;
 fun print_translation (Syntax ({print_trtab, ...}, _)) = apply_tr' print_trtab;
+fun print_rules (Syntax ({print_ruletab, ...}, _)) = Symtab.lookup_list print_ruletab;
 fun print_ast_translation (Syntax ({print_ast_trtab, ...}, _)) = apply_ast_tr' print_ast_trtab;
 fun token_translation (Syntax ({tokentrtab, ...}, _)) = lookup_tokentr tokentrtab;
 
+fun prtabs (Syntax ({prtabs, ...}, _)) = prtabs;
+
 type mode = string * bool;
 val mode_default = ("", true);
 val mode_input = (Print_Mode.input, true);
diff -r f427c9890c46 -r 097c93dcd877 src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Wed Apr 06 17:00:40 2011 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Wed Apr 06 17:15:06 2011 +0200
@@ -268,12 +268,11 @@
   let
     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 tr;
+    val parse_rules = Syntax.parse_rules syn;
   in
     parse_asts ctxt false root input
-    |> (map o apsnd o Exn.maps_result) (norm #> Exn.interruptible_capture ast_to_term)
+    |> (map o apsnd o Exn.maps_result)
+        (Ast.normalize ctxt parse_rules #> Exn.interruptible_capture (ast_to_term ctxt tr))
   end;
 
 
@@ -557,14 +556,11 @@
 fun unparse_t t_to_ast prt_t markup ctxt curried t =
   let
     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, prtabs, ...} = Syntax.rep_syntax syn;
   in
-    t_to_ast ctxt tr' t
-    |> Ast.normalize ctxt (Symtab.lookup_list print_ruletab)
-    |> prt_t ctxt curried prtabs ast_tr' tokentr
+    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
     |> Pretty.markup markup
   end;