fixed diagnostic output of print modes;

--- a/src/Pure/Syntax/printer.ML	Fri Apr 04 16:33:28 1997 +0200
+++ b/src/Pure/Syntax/printer.ML	Fri Apr 04 19:07:54 1997 +0200
@@ -20,7 +20,6 @@
   val term_to_ast: (string -> (typ -> term list -> term) option) -> term -> Ast.ast
   val typ_to_ast: (string -> (typ -> term list -> term) option) -> typ -> Ast.ast
   type prtabs
-  val prmodes_of: prtabs -> string list
   val empty_prtabs: prtabs
   val extend_prtabs: prtabs -> string -> SynExt.xprod list -> prtabs
   val merge_prtabs: prtabs -> prtabs -> prtabs
@@ -177,8 +176,6 @@
 
 type prtabs = (string * ((symb list * int * int) list) Symtab.table) list;
 
-fun prmodes_of prtabs = filter_out (equal "") (map fst prtabs);
-
 (*find tab for mode*)
 fun get_tab prtabs mode =
   if_none (assoc (prtabs, mode)) Symtab.null;

--- a/src/Pure/Syntax/symbol_font.ML	Fri Apr 04 16:33:28 1997 +0200
+++ b/src/Pure/Syntax/symbol_font.ML	Fri Apr 04 19:07:54 1997 +0200
@@ -11,8 +11,11 @@
   val char: string -> string option
   val name: string -> string option
   val read_charnames: string list -> string list
-  val write_charnames:  string list -> string list	(*normal backslashes*)
-  val write_charnames':  string list -> string list	(*escaped backslashes*)
+  val read_chnames: string -> string
+  val write_charnames: string list -> string list	(*normal backslashes*)
+  val write_chnames: string -> string
+  val write_charnames': string list -> string list	(*escaped backslashes*)
+  val write_chnames': string -> string
 end;
 
 
@@ -78,6 +81,8 @@
   fun read_charnames chs =
     if forall (not_equal "\\") chs then chs
     else #1 (repeat (scan_symbol || scan_one (K true)) chs);
+
+  val read_chnames = implode o read_charnames o explode;
 end;
 
 
@@ -95,5 +100,7 @@
 val write_charnames = write_chars "";
 val write_charnames' = write_chars "\\";
 
+val write_chnames = implode o write_charnames o explode;
+val write_chnames' = implode o write_charnames' o explode;
 
 end;

--- a/src/Pure/Syntax/syn_ext.ML	Fri Apr 04 16:33:28 1997 +0200
+++ b/src/Pure/Syntax/syn_ext.ML	Fri Apr 04 19:07:54 1997 +0200
@@ -35,6 +35,7 @@
       logtypes: string list,
       xprods: xprod list,
       consts: string list,
+      prmodes: string list,
       parse_ast_translation: (string * (Ast.ast list -> Ast.ast)) list,
       parse_rules: (Ast.ast * Ast.ast) list,
       parse_translation: (string * (term list -> term)) list,
@@ -286,13 +287,14 @@
     logtypes: string list,
     xprods: xprod list,
     consts: string list,
+    prmodes: string list,
     parse_ast_translation: (string * (Ast.ast list -> Ast.ast)) list,
     parse_rules: (Ast.ast * Ast.ast) list,
     parse_translation: (string * (term list -> term)) list,
     print_translation: (string * (typ -> term list -> term)) list,
     print_rules: (Ast.ast * Ast.ast) list,
     print_ast_translation: (string * (Ast.ast list -> Ast.ast)) list,
-    token_translation: (string * string * (string -> string * int)) list};
+    token_translation: (string * string * (string -> string * int)) list}
 
 
 (* syn_ext *)
@@ -311,6 +313,7 @@
       logtypes = logtypes',
       xprods = xprods,
       consts = filter is_xid (consts union mfix_consts),
+      prmodes = distinct (map (fn (m, _, _) => m) tokentrfuns),
       parse_ast_translation = parse_ast_translation,
       parse_rules = parse_rules,
       parse_translation = parse_translation,

--- 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;