# HG changeset patch
# User wenzelm
# Date 850219322 -3600
# Node ID a163d2be1bb5b933230211fc1c88cf9ad4a701a4
# Parent  38295260a740cf66659672a0db5ff4b57bf4a54d
added chartrans;
prmode: added 'inout' option;

diff -r 38295260a740 -r a163d2be1bb5 src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Tue Dec 10 13:00:52 1996 +0100
+++ b/src/Pure/Syntax/syntax.ML	Tue Dec 10 13:02:02 1996 +0100
@@ -31,7 +31,7 @@
   type syntax
   val extend_log_types: syntax -> string list -> syntax
   val extend_type_gram: syntax -> (string * int * mixfix) list -> syntax
-  val extend_const_gram: syntax -> string -> (string * typ * mixfix) list -> syntax
+  val extend_const_gram: syntax -> string * bool -> (string * typ * mixfix) list -> syntax
   val extend_consts: syntax -> string list -> syntax
   val extend_trfuns: syntax ->
     (string * (ast list -> ast)) list *
@@ -57,6 +57,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;
 
 structure Syntax : SYNTAX =
@@ -124,6 +125,7 @@
 
 datatype syntax =
   Syntax of {
+    chartrans: (string * string) list,
     lexicon: lexicon,
     logtypes: string list,
     gram: gram,
@@ -141,6 +143,7 @@
 
 val empty_syntax =
   Syntax {
+    chartrans = [],
     lexicon = empty_lexicon,
     logtypes = [],
     gram = empty_gram,
@@ -156,19 +159,21 @@
 
 (* extend_syntax *)
 
-fun extend_syntax prmode (Syntax tabs) syn_ext =
+fun extend_syntax (mode, inout) (Syntax tabs) syn_ext =
   let
-    val {lexicon, logtypes = logtypes1, gram, consts = consts1, parse_ast_trtab,
-      parse_ruletab, parse_trtab, print_trtab, print_ruletab, print_ast_trtab,
-      prtabs} = tabs;
+    val {chartrans = _, 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 {
-      lexicon = if prmode = "" then extend_lexicon lexicon (delims_of xprods) else lexicon,
+      chartrans = chartrans_of prtabs',
+      lexicon = if inout then extend_lexicon lexicon (delims_of xprods) else lexicon,
       logtypes = extend_list logtypes1 logtypes2,
-      gram = if prmode = "" then extend_gram gram xprods else gram,
+      gram = if inout then extend_gram gram xprods else gram,
       consts = consts2 union consts1,
       parse_ast_trtab =
         extend_trtab parse_ast_trtab parse_ast_translation "parse ast translation",
@@ -178,7 +183,7 @@
       print_ruletab = extend_ruletab print_ruletab print_rules,
       print_ast_trtab =
         extend_trtab print_ast_trtab print_ast_translation "print ast translation",
-      prtabs = extend_prtabs prtabs prmode xprods}
+      prtabs = prtabs'}
   end;
 
 
@@ -186,19 +191,21 @@
 
 fun merge_syntaxes (Syntax tabs1) (Syntax tabs2) =
   let
-    val {lexicon = lexicon1, logtypes = logtypes1, gram = gram1, consts = consts1,
-      parse_ast_trtab = parse_ast_trtab1, parse_ruletab = parse_ruletab1,
+    val {chartrans = _, 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 {lexicon = lexicon2, logtypes = logtypes2, gram = gram2, consts = consts2,
-      parse_ast_trtab = parse_ast_trtab2, parse_ruletab = parse_ruletab2,
+    val {chartrans = _, 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,
@@ -211,14 +218,14 @@
       print_ruletab = merge_ruletabs print_ruletab1 print_ruletab2,
       print_ast_trtab =
         merge_trtabs print_ast_trtab1 print_ast_trtab2 "print ast translation",
-      prtabs = merge_prtabs prtabs1 prtabs2}
+      prtabs = prtabs}
   end;
 
 
 (* type_syn *)
 
-val type_syn = extend_syntax "" empty_syntax type_ext;
-val pure_syn = extend_syntax "" type_syn pure_ext;
+val type_syn = extend_syntax ("", true) empty_syntax type_ext;
+val pure_syn = extend_syntax ("", true) type_syn pure_ext;
 
 
 (** inspect syntax **)
@@ -231,8 +238,12 @@
 
 fun print_gram (Syntax tabs) =
   let
-    val {lexicon, logtypes, gram, prtabs, ...} = tabs;
+    val pretty_chartrans =
+      map (fn (c, s) => Pretty.str (c ^ " -> " ^ quote s));
+
+    val {chartrans, 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));
@@ -277,7 +288,8 @@
   let
     val {lexicon, gram, parse_ast_trtab, parse_ruletab, ...} = tabs;
 
-    val toks = tokenize lexicon false str;
+    val chars = SymbolFont.read_charnames (explode str);
+    val toks = tokenize lexicon false chars;
     val _ = writeln ("tokens: " ^ space_implode " " (map display_token toks));
 
     fun show_pt pt =
@@ -300,7 +312,8 @@
   let
     val {lexicon, gram, parse_ast_trtab, logtypes, ...} = tabs;
     val root' = if root mem logtypes then logic else root;
-    val pts = parse gram root' (tokenize lexicon xids str);
+    val chars = SymbolFont.read_charnames (explode str);
+    val pts = parse gram root' (tokenize lexicon xids chars);
 
     fun show_pt pt = writeln (str_of_ast (pt_to_ast (K None) pt));
   in
@@ -419,20 +432,26 @@
 
 
 fun extend_log_types syn logtypes =
-  extend_syntax "" syn (syn_ext_logtypes logtypes);
+  extend_syntax ("", true) syn (syn_ext_logtypes logtypes);
 
-val extend_type_gram = ext_syntax syn_ext_types "";
+val extend_type_gram = ext_syntax syn_ext_types ("", true);
 
 fun extend_const_gram syn prmode = ext_syntax syn_ext_consts prmode syn;
 
-val extend_consts = ext_syntax syn_ext_const_names "";
+val extend_consts = ext_syntax syn_ext_const_names ("", true);
 
-val extend_trfuns = ext_syntax syn_ext_trfuns "";
+val extend_trfuns = ext_syntax syn_ext_trfuns ("", true);
 
 fun extend_trrules syn rules =
-  ext_syntax syn_ext_rules "" syn (prep_rules (read_pattern syn) rules);
+  ext_syntax syn_ext_rules ("", true) syn (prep_rules (read_pattern syn) rules);
 
 fun extend_trrules_i syn rules =
-  ext_syntax syn_ext_rules "" syn (prep_rules I rules);
+  ext_syntax syn_ext_rules ("", true) syn (prep_rules I rules);
+
+
+
+(* FIXME test only *)
+
+fun prtabs_of (Syntax {prtabs, ...}) = prtabs;
 
 end;