fixed diagnostic output of print modes;
authorwenzelm
Fri Apr 04 19:07:54 1997 +0200 (1997-04-04)
changeset 2913ce271fa4d8e2
parent 2912 3fac3e8d5d3e
child 2914 01d24f98528f
fixed diagnostic output of print modes;
src/Pure/Syntax/printer.ML
src/Pure/Syntax/symbol_font.ML
src/Pure/Syntax/syn_ext.ML
src/Pure/Syntax/syntax.ML
     1.1 --- a/src/Pure/Syntax/printer.ML	Fri Apr 04 16:33:28 1997 +0200
     1.2 +++ b/src/Pure/Syntax/printer.ML	Fri Apr 04 19:07:54 1997 +0200
     1.3 @@ -20,7 +20,6 @@
     1.4    val term_to_ast: (string -> (typ -> term list -> term) option) -> term -> Ast.ast
     1.5    val typ_to_ast: (string -> (typ -> term list -> term) option) -> typ -> Ast.ast
     1.6    type prtabs
     1.7 -  val prmodes_of: prtabs -> string list
     1.8    val empty_prtabs: prtabs
     1.9    val extend_prtabs: prtabs -> string -> SynExt.xprod list -> prtabs
    1.10    val merge_prtabs: prtabs -> prtabs -> prtabs
    1.11 @@ -177,8 +176,6 @@
    1.12  
    1.13  type prtabs = (string * ((symb list * int * int) list) Symtab.table) list;
    1.14  
    1.15 -fun prmodes_of prtabs = filter_out (equal "") (map fst prtabs);
    1.16 -
    1.17  (*find tab for mode*)
    1.18  fun get_tab prtabs mode =
    1.19    if_none (assoc (prtabs, mode)) Symtab.null;
     2.1 --- a/src/Pure/Syntax/symbol_font.ML	Fri Apr 04 16:33:28 1997 +0200
     2.2 +++ b/src/Pure/Syntax/symbol_font.ML	Fri Apr 04 19:07:54 1997 +0200
     2.3 @@ -11,8 +11,11 @@
     2.4    val char: string -> string option
     2.5    val name: string -> string option
     2.6    val read_charnames: string list -> string list
     2.7 -  val write_charnames:  string list -> string list	(*normal backslashes*)
     2.8 -  val write_charnames':  string list -> string list	(*escaped backslashes*)
     2.9 +  val read_chnames: string -> string
    2.10 +  val write_charnames: string list -> string list	(*normal backslashes*)
    2.11 +  val write_chnames: string -> string
    2.12 +  val write_charnames': string list -> string list	(*escaped backslashes*)
    2.13 +  val write_chnames': string -> string
    2.14  end;
    2.15  
    2.16  
    2.17 @@ -78,6 +81,8 @@
    2.18    fun read_charnames chs =
    2.19      if forall (not_equal "\\") chs then chs
    2.20      else #1 (repeat (scan_symbol || scan_one (K true)) chs);
    2.21 +
    2.22 +  val read_chnames = implode o read_charnames o explode;
    2.23  end;
    2.24  
    2.25  
    2.26 @@ -95,5 +100,7 @@
    2.27  val write_charnames = write_chars "";
    2.28  val write_charnames' = write_chars "\\";
    2.29  
    2.30 +val write_chnames = implode o write_charnames o explode;
    2.31 +val write_chnames' = implode o write_charnames' o explode;
    2.32  
    2.33  end;
     3.1 --- a/src/Pure/Syntax/syn_ext.ML	Fri Apr 04 16:33:28 1997 +0200
     3.2 +++ b/src/Pure/Syntax/syn_ext.ML	Fri Apr 04 19:07:54 1997 +0200
     3.3 @@ -35,6 +35,7 @@
     3.4        logtypes: string list,
     3.5        xprods: xprod list,
     3.6        consts: string list,
     3.7 +      prmodes: string list,
     3.8        parse_ast_translation: (string * (Ast.ast list -> Ast.ast)) list,
     3.9        parse_rules: (Ast.ast * Ast.ast) list,
    3.10        parse_translation: (string * (term list -> term)) list,
    3.11 @@ -286,13 +287,14 @@
    3.12      logtypes: string list,
    3.13      xprods: xprod list,
    3.14      consts: string list,
    3.15 +    prmodes: string list,
    3.16      parse_ast_translation: (string * (Ast.ast list -> Ast.ast)) list,
    3.17      parse_rules: (Ast.ast * Ast.ast) list,
    3.18      parse_translation: (string * (term list -> term)) list,
    3.19      print_translation: (string * (typ -> term list -> term)) list,
    3.20      print_rules: (Ast.ast * Ast.ast) list,
    3.21      print_ast_translation: (string * (Ast.ast list -> Ast.ast)) list,
    3.22 -    token_translation: (string * string * (string -> string * int)) list};
    3.23 +    token_translation: (string * string * (string -> string * int)) list}
    3.24  
    3.25  
    3.26  (* syn_ext *)
    3.27 @@ -311,6 +313,7 @@
    3.28        logtypes = logtypes',
    3.29        xprods = xprods,
    3.30        consts = filter is_xid (consts union mfix_consts),
    3.31 +      prmodes = distinct (map (fn (m, _, _) => m) tokentrfuns),
    3.32        parse_ast_translation = parse_ast_translation,
    3.33        parse_rules = parse_rules,
    3.34        parse_translation = parse_translation,
     4.1 --- a/src/Pure/Syntax/syntax.ML	Fri Apr 04 16:33:28 1997 +0200
     4.2 +++ b/src/Pure/Syntax/syntax.ML	Fri Apr 04 19:07:54 1997 +0200
     4.3 @@ -168,6 +168,7 @@
     4.4      logtypes: string list,
     4.5      gram: gram,
     4.6      consts: string list,
     4.7 +    prmodes: string list,
     4.8      parse_ast_trtab: ast trtab,
     4.9      parse_ruletab: ruletab,
    4.10      parse_trtab: term trtab,
    4.11 @@ -175,7 +176,7 @@
    4.12      print_ruletab: ruletab,
    4.13      print_ast_trtab: ast trtab,
    4.14      tokentrtab: (string * (string * ((string -> string * int) * stamp)) list) list,
    4.15 -    prtabs: prtabs};
    4.16 +    prtabs: prtabs}
    4.17  
    4.18  
    4.19  (* empty_syntax *)
    4.20 @@ -186,6 +187,7 @@
    4.21      logtypes = [],
    4.22      gram = empty_gram,
    4.23      consts = [],
    4.24 +    prmodes = [],
    4.25      parse_ast_trtab = empty_trtab,
    4.26      parse_ruletab = empty_ruletab,
    4.27      parse_trtab = empty_trtab,
    4.28 @@ -193,18 +195,18 @@
    4.29      print_ruletab = empty_ruletab,
    4.30      print_ast_trtab = empty_trtab,
    4.31      tokentrtab = [],
    4.32 -    prtabs = empty_prtabs};
    4.33 +    prtabs = empty_prtabs}
    4.34  
    4.35  
    4.36  (* extend_syntax *)
    4.37  
    4.38  fun extend_syntax (mode, inout) (Syntax tabs) syn_ext =
    4.39    let
    4.40 -    val {lexicon, logtypes = logtypes1, gram, consts = consts1,
    4.41 +    val {lexicon, logtypes = logtypes1, gram, consts = consts1, prmodes = prmodes1,
    4.42        parse_ast_trtab, parse_ruletab, parse_trtab, print_trtab, print_ruletab,
    4.43        print_ast_trtab, tokentrtab, prtabs} = tabs;
    4.44 -    val SynExt {logtypes = logtypes2, xprods, consts = consts2, parse_ast_translation,
    4.45 -      parse_rules, parse_translation, print_translation, print_rules,
    4.46 +    val SynExt {logtypes = logtypes2, xprods, consts = consts2, prmodes = prmodes2,
    4.47 +      parse_ast_translation, parse_rules, parse_translation, print_translation, print_rules,
    4.48        print_ast_translation, token_translation} = syn_ext;
    4.49    in
    4.50      Syntax {
    4.51 @@ -212,6 +214,7 @@
    4.52        logtypes = extend_list logtypes1 logtypes2,
    4.53        gram = if inout then extend_gram gram xprods else gram,
    4.54        consts = consts2 union consts1,
    4.55 +      prmodes = (mode ins prmodes2) union prmodes1,
    4.56        parse_ast_trtab =
    4.57          extend_trtab parse_ast_trtab parse_ast_translation "parse ast translation",
    4.58        parse_ruletab = extend_ruletab parse_ruletab parse_rules,
    4.59 @@ -229,14 +232,14 @@
    4.60  
    4.61  fun merge_syntaxes (Syntax tabs1) (Syntax tabs2) =
    4.62    let
    4.63 -    val {lexicon = lexicon1, logtypes = logtypes1, gram = gram1,
    4.64 -      consts = consts1, parse_ast_trtab = parse_ast_trtab1, parse_ruletab = parse_ruletab1,
    4.65 +    val {lexicon = lexicon1, logtypes = logtypes1, gram = gram1, consts = consts1,
    4.66 +      prmodes = prmodes1, parse_ast_trtab = parse_ast_trtab1, parse_ruletab = parse_ruletab1,
    4.67        parse_trtab = parse_trtab1, print_trtab = print_trtab1,
    4.68        print_ruletab = print_ruletab1, print_ast_trtab = print_ast_trtab1,
    4.69        tokentrtab = tokentrtab1, prtabs = prtabs1} = tabs1;
    4.70  
    4.71 -    val {lexicon = lexicon2, logtypes = logtypes2, gram = gram2,
    4.72 -      consts = consts2, parse_ast_trtab = parse_ast_trtab2, parse_ruletab = parse_ruletab2,
    4.73 +    val {lexicon = lexicon2, logtypes = logtypes2, gram = gram2, consts = consts2,
    4.74 +      prmodes = prmodes2, parse_ast_trtab = parse_ast_trtab2, parse_ruletab = parse_ruletab2,
    4.75        parse_trtab = parse_trtab2, print_trtab = print_trtab2,
    4.76        print_ruletab = print_ruletab2, print_ast_trtab = print_ast_trtab2,
    4.77        tokentrtab = tokentrtab2, prtabs = prtabs2} = tabs2;
    4.78 @@ -246,6 +249,7 @@
    4.79        logtypes = merge_lists logtypes1 logtypes2,
    4.80        gram = merge_grams gram1 gram2,
    4.81        consts = merge_lists consts1 consts2,
    4.82 +      prmodes = merge_lists prmodes1 prmodes2,
    4.83        parse_ast_trtab =
    4.84          merge_trtabs parse_ast_trtab1 parse_ast_trtab2 "parse ast translation",
    4.85        parse_ruletab = merge_ruletabs parse_ruletab1 parse_ruletab2,
    4.86 @@ -277,12 +281,13 @@
    4.87  
    4.88  fun print_gram (Syntax tabs) =
    4.89    let
    4.90 -    val {lexicon, logtypes, gram, prtabs, ...} = tabs;
    4.91 +    val {lexicon, logtypes, prmodes, gram, prtabs, ...} = tabs;
    4.92 +    val prmodes' = sort_strings (filter_out (equal "") prmodes);
    4.93    in
    4.94      Pretty.writeln (pretty_strs_qs "lexicon:" (dest_lexicon lexicon));
    4.95      Pretty.writeln (Pretty.strs ("logtypes:" :: logtypes));
    4.96      Pretty.writeln (Pretty.big_list "prods:" (pretty_gram gram));
    4.97 -    Pretty.writeln (pretty_strs_qs "print modes:" (prmodes_of prtabs))
    4.98 +    Pretty.writeln (pretty_strs_qs "print modes:" prmodes')
    4.99    end;
   4.100  
   4.101