TableFun: renamed xxx_multi to xxx_list;
authorwenzelm
Mon Feb 06 20:59:57 2006 +0100 (2006-02-06 ago)
changeset 189578c3abd63bce3
parent 18956 c050ae1f8f52
child 18958 9151a29d2864
TableFun: renamed xxx_multi to xxx_list;
tuned;
src/Pure/Syntax/printer.ML
src/Pure/type.ML
     1.1 --- a/src/Pure/Syntax/printer.ML	Mon Feb 06 20:59:56 2006 +0100
     1.2 +++ b/src/Pure/Syntax/printer.ML	Mon Feb 06 20:59:57 2006 +0100
     1.3 @@ -191,7 +191,7 @@
     1.4  
     1.5  type prtabs = (string * ((symb list * int * int) list) Symtab.table) list;
     1.6  
     1.7 -fun mode_tab prtabs mode = if_none (AList.lookup (op =) prtabs mode) Symtab.empty;
     1.8 +fun mode_tab prtabs mode = the_default Symtab.empty (AList.lookup (op =) prtabs mode);
     1.9  fun mode_tabs prtabs modes = List.mapPartial (AList.lookup (op =) prtabs) (modes @ [""]);
    1.10  
    1.11  
    1.12 @@ -248,13 +248,13 @@
    1.13      val tab = fold f fmts (mode_tab prtabs mode);
    1.14    in AList.update (op =) (mode, tab) prtabs end;
    1.15  
    1.16 -fun extend_prtabs m = change_prtabs Symtab.update_multi m;
    1.17 -fun remove_prtabs m = change_prtabs (Symtab.remove_multi (op =)) m;
    1.18 +fun extend_prtabs m = change_prtabs Symtab.update_list m;
    1.19 +fun remove_prtabs m = change_prtabs (Symtab.remove_list (op =)) m;
    1.20  
    1.21  fun merge_prtabs prtabs1 prtabs2 =
    1.22    let
    1.23      val modes = distinct (map fst (prtabs1 @ prtabs2));
    1.24 -    fun merge m = (m, Symtab.merge_multi' (op =) (mode_tab prtabs1 m, mode_tab prtabs2 m));
    1.25 +    fun merge m = (m, Symtab.merge_list (op =) (mode_tab prtabs1 m, mode_tab prtabs2 m));
    1.26    in map merge modes end;
    1.27  
    1.28  
    1.29 @@ -330,7 +330,7 @@
    1.30  
    1.31          (*find matching table entry, or print as prefix / postfix*)
    1.32          fun prnt ([], []) = prefixT tup
    1.33 -          | prnt ([], tb :: tbs) = prnt (Symtab.lookup_multi tb a, tbs)
    1.34 +          | prnt ([], tb :: tbs) = prnt (Symtab.lookup_list tb a, tbs)
    1.35            | prnt ((pr, n, p') :: prnps, tbs) =
    1.36                if nargs = n then parT (pr, args, p, p')
    1.37                else if nargs > n andalso not type_mode then
     2.1 --- a/src/Pure/type.ML	Mon Feb 06 20:59:56 2006 +0100
     2.2 +++ b/src/Pure/type.ML	Mon Feb 06 20:59:57 2006 +0100
     2.3 @@ -151,7 +151,7 @@
     2.4  local
     2.5  
     2.6  fun inst_typ env (Type (c, Ts)) = Type (c, map (inst_typ env) Ts)
     2.7 -  | inst_typ env (T as TFree (x, _)) = if_none (AList.lookup (op =) env x) T
     2.8 +  | inst_typ env (T as TFree (x, _)) = the_default T (AList.lookup (op =) env x)
     2.9    | inst_typ _ T = T;
    2.10  
    2.11  fun certify_typ normalize syntax tsig ty =
    2.12 @@ -487,7 +487,7 @@
    2.13  
    2.14  fun insert_arities pp classes (t, ars) arities =
    2.15    let val ars' =
    2.16 -    Symtab.lookup_multi arities t
    2.17 +    Symtab.lookup_list arities t
    2.18      |> fold_rev (fold_rev (insert pp classes t)) (map (complete classes) ars)
    2.19    in Symtab.update (t, ars') arities end;
    2.20