src/Pure/Syntax/syntax.ML

--- a/src/Pure/Syntax/syntax.ML	Fri Apr 04 16:33:28 1997 +0200
+++ b/src/Pure/Syntax/syntax.ML	Fri Apr 04 19:07:54 1997 +0200
@@ -168,6 +168,7 @@
     logtypes: string list,
     gram: gram,
     consts: string list,
+    prmodes: string list,
     parse_ast_trtab: ast trtab,
     parse_ruletab: ruletab,
     parse_trtab: term trtab,
@@ -175,7 +176,7 @@
     print_ruletab: ruletab,
     print_ast_trtab: ast trtab,
     tokentrtab: (string * (string * ((string -> string * int) * stamp)) list) list,
-    prtabs: prtabs};
+    prtabs: prtabs}
 
 
 (* empty_syntax *)
@@ -186,6 +187,7 @@
     logtypes = [],
     gram = empty_gram,
     consts = [],
+    prmodes = [],
     parse_ast_trtab = empty_trtab,
     parse_ruletab = empty_ruletab,
     parse_trtab = empty_trtab,
@@ -193,18 +195,18 @@
     print_ruletab = empty_ruletab,
     print_ast_trtab = empty_trtab,
     tokentrtab = [],
-    prtabs = empty_prtabs};
+    prtabs = empty_prtabs}
 
 
 (* extend_syntax *)
 
 fun extend_syntax (mode, inout) (Syntax tabs) syn_ext =
   let
-    val {lexicon, logtypes = logtypes1, gram, consts = consts1,
+    val {lexicon, logtypes = logtypes1, gram, consts = consts1, prmodes = prmodes1,
       parse_ast_trtab, parse_ruletab, parse_trtab, print_trtab, print_ruletab,
       print_ast_trtab, tokentrtab, prtabs} = tabs;
-    val SynExt {logtypes = logtypes2, xprods, consts = consts2, parse_ast_translation,
-      parse_rules, parse_translation, print_translation, print_rules,
+    val SynExt {logtypes = logtypes2, xprods, consts = consts2, prmodes = prmodes2,
+      parse_ast_translation, parse_rules, parse_translation, print_translation, print_rules,
       print_ast_translation, token_translation} = syn_ext;
   in
     Syntax {
@@ -212,6 +214,7 @@
       logtypes = extend_list logtypes1 logtypes2,
       gram = if inout then extend_gram gram xprods else gram,
       consts = consts2 union consts1,
+      prmodes = (mode ins prmodes2) union prmodes1,
       parse_ast_trtab =
         extend_trtab parse_ast_trtab parse_ast_translation "parse ast translation",
       parse_ruletab = extend_ruletab parse_ruletab parse_rules,
@@ -229,14 +232,14 @@
 
 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 {lexicon = lexicon1, logtypes = logtypes1, gram = gram1, consts = consts1,
+      prmodes = prmodes1, 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,
       tokentrtab = tokentrtab1, prtabs = prtabs1} = tabs1;
 
-    val {lexicon = lexicon2, logtypes = logtypes2, gram = gram2,
-      consts = consts2, parse_ast_trtab = parse_ast_trtab2, parse_ruletab = parse_ruletab2,
+    val {lexicon = lexicon2, logtypes = logtypes2, gram = gram2, consts = consts2,
+      prmodes = prmodes2, 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,
       tokentrtab = tokentrtab2, prtabs = prtabs2} = tabs2;
@@ -246,6 +249,7 @@
       logtypes = merge_lists logtypes1 logtypes2,
       gram = merge_grams gram1 gram2,
       consts = merge_lists consts1 consts2,
+      prmodes = merge_lists prmodes1 prmodes2,
       parse_ast_trtab =
         merge_trtabs parse_ast_trtab1 parse_ast_trtab2 "parse ast translation",
       parse_ruletab = merge_ruletabs parse_ruletab1 parse_ruletab2,
@@ -277,12 +281,13 @@
 
 fun print_gram (Syntax tabs) =
   let
-    val {lexicon, logtypes, gram, prtabs, ...} = tabs;
+    val {lexicon, logtypes, prmodes, gram, prtabs, ...} = tabs;
+    val prmodes' = sort_strings (filter_out (equal "") prmodes);
   in
     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 "print modes:" (prmodes_of prtabs))
+    Pretty.writeln (pretty_strs_qs "print modes:" prmodes')
   end;