# HG changeset patch
# User wenzelm
# Date 850494872 -3600
# Node ID 4127499d9b525b1ec1661a9a264b4f8803a37c12
# Parent  e7c2bce815ba76c0cb95b6326cac2ac38d29610a
added extend_trfunsT;
removed test: prtabs_of;
removed chartrans;

diff -r e7c2bce815ba -r 4127499d9b52 src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Fri Dec 13 17:30:28 1996 +0100
+++ b/src/Pure/Syntax/syntax.ML	Fri Dec 13 17:34:32 1996 +0100
@@ -8,15 +8,15 @@
 infix |-> <-| <->;
 
 signature BASIC_SYNTAX =
-  sig
+sig
   include AST0
   include SYN_TRANS0
   include MIXFIX0
   include PRINTER0
-  end;
+end;
 
 signature SYNTAX =
-  sig
+sig
   include AST1
   include LEXICON0
   include SYN_EXT0
@@ -38,6 +38,7 @@
     (string * (term list -> term)) list *
     (string * (term list -> term)) list *
     (string * (ast list -> ast)) list -> syntax
+  val extend_trfunsT: syntax -> (string * (typ -> term list -> term)) list -> syntax
   val extend_trrules: syntax -> (string * string) trrule list -> syntax
   val extend_trrules_i: syntax -> ast trrule list -> syntax
   val merge_syntaxes: syntax -> syntax -> syntax
@@ -57,8 +58,7 @@
   val simple_string_of_typ: typ -> string
   val simple_pprint_typ: typ -> pprint_args -> unit
   val ambiguity_level: int ref
-  val prtabs_of: syntax -> Printer.prtabs   (* FIXME test only *)
-  end;
+end;
 
 structure Syntax : SYNTAX =
 struct
@@ -69,6 +69,7 @@
 (** tables of translation functions **)
 
 (*the ref serves as unique id*)
+(*does not subsume typed print translations*)
 type 'a trtab = (('a list -> 'a) * unit ref) Symtab.table;
 
 val dest_trtab = Symtab.dest;
@@ -125,7 +126,6 @@
 
 datatype syntax =
   Syntax of {
-    chartrans: (string * string) list,
     lexicon: lexicon,
     logtypes: string list,
     gram: gram,
@@ -133,7 +133,7 @@
     parse_ast_trtab: ast trtab,
     parse_ruletab: ruletab,
     parse_trtab: term trtab,
-    print_trtab: term trtab,
+    print_trtab: ((typ -> term list -> term) * unit ref) Symtab.table,
     print_ruletab: ruletab,
     print_ast_trtab: ast trtab,
     prtabs: prtabs};
@@ -143,7 +143,6 @@
 
 val empty_syntax =
   Syntax {
-    chartrans = [],
     lexicon = empty_lexicon,
     logtypes = [],
     gram = empty_gram,
@@ -161,16 +160,14 @@
 
 fun extend_syntax (mode, inout) (Syntax tabs) syn_ext =
   let
-    val {chartrans = _, lexicon, logtypes = logtypes1, gram, consts = consts1,
+    val {lexicon, logtypes = logtypes1, gram, consts = consts1,
       parse_ast_trtab, parse_ruletab, parse_trtab, print_trtab, print_ruletab,
       print_ast_trtab, prtabs} = tabs;
     val SynExt {logtypes = logtypes2, xprods, consts = consts2, parse_ast_translation,
       parse_rules, parse_translation, print_translation, print_rules,
       print_ast_translation} = syn_ext;
-    val prtabs' = extend_prtabs prtabs mode xprods;
   in
     Syntax {
-      chartrans = chartrans_of prtabs',
       lexicon = if inout then extend_lexicon lexicon (delims_of xprods) else lexicon,
       logtypes = extend_list logtypes1 logtypes2,
       gram = if inout then extend_gram gram xprods else gram,
@@ -183,7 +180,7 @@
       print_ruletab = extend_ruletab print_ruletab print_rules,
       print_ast_trtab =
         extend_trtab print_ast_trtab print_ast_translation "print ast translation",
-      prtabs = prtabs'}
+      prtabs = extend_prtabs prtabs mode xprods}
   end;
 
 
@@ -191,21 +188,19 @@
 
 fun merge_syntaxes (Syntax tabs1) (Syntax tabs2) =
   let
-    val {chartrans = _, lexicon = lexicon1, logtypes = logtypes1, gram = gram1,
+    val {lexicon = lexicon1, logtypes = logtypes1, gram = gram1,
       consts = consts1, parse_ast_trtab = parse_ast_trtab1, parse_ruletab = parse_ruletab1,
       parse_trtab = parse_trtab1, print_trtab = print_trtab1,
       print_ruletab = print_ruletab1, print_ast_trtab = print_ast_trtab1,
       prtabs = prtabs1} = tabs1;
 
-    val {chartrans = _, lexicon = lexicon2, logtypes = logtypes2, gram = gram2,
+    val {lexicon = lexicon2, logtypes = logtypes2, gram = gram2,
       consts = consts2, parse_ast_trtab = parse_ast_trtab2, parse_ruletab = parse_ruletab2,
       parse_trtab = parse_trtab2, print_trtab = print_trtab2,
       print_ruletab = print_ruletab2, print_ast_trtab = print_ast_trtab2,
       prtabs = prtabs2} = tabs2;
-    val prtabs = merge_prtabs prtabs1 prtabs2;
   in
     Syntax {
-      chartrans = chartrans_of prtabs,
       lexicon = merge_lexicons lexicon1 lexicon2,
       logtypes = merge_lists logtypes1 logtypes2,
       gram = merge_grams gram1 gram2,
@@ -218,7 +213,7 @@
       print_ruletab = merge_ruletabs print_ruletab1 print_ruletab2,
       print_ast_trtab =
         merge_trtabs print_ast_trtab1 print_ast_trtab2 "print ast translation",
-      prtabs = prtabs}
+      prtabs = merge_prtabs prtabs1 prtabs2}
   end;
 
 
@@ -238,16 +233,12 @@
 
 fun print_gram (Syntax tabs) =
   let
-    val pretty_chartrans =
-      map (fn (c, s) => Pretty.str (c ^ " -> " ^ quote s));
-
-    val {chartrans, lexicon, logtypes, gram, prtabs, ...} = tabs;
+    val {lexicon, logtypes, gram, prtabs, ...} = tabs;
   in
-    Pretty.writeln (Pretty.big_list "chartrans:" (pretty_chartrans chartrans));
     Pretty.writeln (pretty_strs_qs "lexicon:" (dest_lexicon lexicon));
     Pretty.writeln (Pretty.strs ("logtypes:" :: logtypes));
     Pretty.writeln (Pretty.big_list "prods:" (pretty_gram gram));
-    Pretty.writeln (pretty_strs_qs "printer modes:" (prmodes_of prtabs))
+    Pretty.writeln (pretty_strs_qs "print modes:" (prmodes_of prtabs))
   end;
 
 
@@ -442,6 +433,8 @@
 
 val extend_trfuns = ext_syntax syn_ext_trfuns ("", true);
 
+val extend_trfunsT = ext_syntax syn_ext_trfunsT ("", true);
+
 fun extend_trrules syn rules =
   ext_syntax syn_ext_rules ("", true) syn (prep_rules (read_pattern syn) rules);
 
@@ -449,9 +442,4 @@
   ext_syntax syn_ext_rules ("", true) syn (prep_rules I rules);
 
 
-
-(* FIXME test only *)
-
-fun prtabs_of (Syntax {prtabs, ...}) = prtabs;
-
 end;