1.1 --- a/src/Pure/Syntax/syntax.ML	Sun Apr 17 19:38:53 2005 +0200
     1.2 +++ b/src/Pure/Syntax/syntax.ML	Sun Apr 17 19:39:11 2005 +0200
     1.3 @@ -87,10 +87,7 @@
     1.4  fun extend_trtab name trfuns tab = Symtab.extend (tab, trfuns)
     1.5    handle Symtab.DUPS cs => err_dup_trfuns name cs;
     1.6  
     1.7 -fun remove_trtab trfuns = trfuns |> fold (fn (c, (_, s: stamp)) => fn tab =>
     1.8 -  if Option.map snd (Symtab.lookup (tab, c)) = SOME s
     1.9 -  then Symtab.delete c tab
    1.10 -  else tab);
    1.11 +fun remove_trtab trfuns = fold (Symtab.remove SynExt.eq_trfun) trfuns;
    1.12  
    1.13  fun merge_trtabs name tab1 tab2 = Symtab.merge SynExt.eq_trfun (tab1, tab2)
    1.14    handle Symtab.DUPS cs => err_dup_trfuns name cs;
    1.15 @@ -99,12 +96,8 @@
    1.16  (* print (ast) translations *)
    1.17  
    1.18  fun lookup_tr' tab c = map fst (Symtab.lookup_multi (tab, c));
    1.19 -
    1.20 -fun extend_tr'tab trfuns tab = foldr Symtab.update_multi tab trfuns;
    1.21 -
    1.22 -fun remove_tr'tab trfuns = trfuns |> fold (fn (c, tr) =>
    1.23 -  Symtab.map_entry c (gen_remove SynExt.eq_trfun tr));
    1.24 -
    1.25 +fun extend_tr'tab trfuns = fold_rev (curry Symtab.update_multi) trfuns;
    1.26 +fun remove_tr'tab trfuns = fold (Symtab.remove_multi SynExt.eq_trfun) trfuns;
    1.27  fun merge_tr'tabs tab1 tab2 = Symtab.merge_multi' SynExt.eq_trfun (tab1, tab2);
    1.28  
    1.29  
    1.30 @@ -138,11 +131,9 @@
    1.31  
    1.32  fun extend_tokentrtab tokentrs tabs =
    1.33    let
    1.34 -    fun ins_tokentr (ts, (m, c, f)) =
    1.35 +    fun ins_tokentr (m, c, f) ts =
    1.36        overwrite (ts, (m, ("_" ^ c, (f, stamp ())) :: assocs ts m));
    1.37 -  in
    1.38 -    merge_tokentrtabs tabs (Library.foldl ins_tokentr ([], tokentrs))
    1.39 -  end;
    1.40 +  in merge_tokentrtabs tabs (fold ins_tokentr tokentrs []) end;
    1.41  
    1.42  
    1.43  
    1.44 @@ -156,10 +147,10 @@
    1.45  
    1.46  (* empty, extend, merge ruletabs *)
    1.47  
    1.48 -fun extend_ruletab rules tab =
    1.49 -  foldr Symtab.update_multi tab (map (fn r => (Ast.head_of_rule r, r)) rules);
    1.50 +val extend_ruletab =
    1.51 +  fold_rev (fn r => fn tab => Symtab.update_multi ((Ast.head_of_rule r, r), tab));
    1.52  
    1.53 -val remove_ruletab = fold (fn r => Symtab.map_entry (Ast.head_of_rule r) (remove r));
    1.54 +val remove_ruletab = fold (fn r => Symtab.remove_multi (op =) (Ast.head_of_rule r, r));
    1.55  
    1.56  fun merge_ruletabs tab1 tab2 = Symtab.merge_multi' (op =) (tab1, tab2);
    1.57  
    1.58 @@ -246,7 +237,7 @@
    1.59      val {input, lexicon, gram, consts, prmodes,
    1.60        parse_ast_trtab, parse_ruletab, parse_trtab, print_trtab, print_ruletab,
    1.61        print_ast_trtab, tokentrtab, prtabs} = tabs;
    1.62 -    val input' = if inout then fold remove xprods input else input;
    1.63 +    val input' = if inout then fold (remove (op =)) xprods input else input;
    1.64    in
    1.65      Syntax {
    1.66        input = input',
    1.67 @@ -306,15 +297,14 @@
    1.68  
    1.69  
    1.70  
    1.71 -(** inspect syntax **)
    1.72 +(** print syntax **)
    1.73 +
    1.74 +local
    1.75  
    1.76  fun pretty_strs_qs name strs =
    1.77    Pretty.strs (name :: map Library.quote (sort_strings strs));
    1.78  
    1.79 -
    1.80 -(* print_gram *)
    1.81 -
    1.82 -fun print_gram (Syntax tabs) =
    1.83 +fun pretty_gram (Syntax tabs) =
    1.84    let
    1.85      val {lexicon, prmodes, gram, prtabs, ...} = tabs;
    1.86      val prmodes' = sort_strings (filter_out (equal "") prmodes);
    1.87 @@ -322,13 +312,9 @@
    1.88      [pretty_strs_qs "lexicon:" (Scan.dest_lexicon lexicon),
    1.89        Pretty.big_list "prods:" (Parser.pretty_gram gram),
    1.90        pretty_strs_qs "print modes:" prmodes']
    1.91 -    |> Pretty.chunks |> Pretty.writeln
    1.92    end;
    1.93  
    1.94 -
    1.95 -(* print_trans *)
    1.96 -
    1.97 -fun print_trans (Syntax tabs) =
    1.98 +fun pretty_trans (Syntax tabs) =
    1.99    let
   1.100      fun pretty_trtab name tab =
   1.101        pretty_strs_qs name (Symtab.keys tab);
   1.102 @@ -349,13 +335,15 @@
   1.103        pretty_ruletab "print_rules:" print_ruletab,
   1.104        pretty_trtab "print_ast_translation:" print_ast_trtab,
   1.105        Pretty.big_list "token_translation:" (map pretty_tokentr tokentrtab)]
   1.106 -    |> Pretty.chunks |> Pretty.writeln
   1.107    end;
   1.108  
   1.109 +in
   1.110  
   1.111 -(* print_syntax *)
   1.112 +fun print_gram syn = Pretty.writeln (Pretty.chunks (pretty_gram syn));
   1.113 +fun print_trans syn = Pretty.writeln (Pretty.chunks (pretty_trans syn));
   1.114 +fun print_syntax syn = Pretty.writeln (Pretty.chunks (pretty_gram syn @ pretty_trans syn));
   1.115  
   1.116 -fun print_syntax syn = (print_gram syn; print_trans syn);
   1.117 +end;
   1.118  
   1.119  
   1.120