renamed (is_)null to (is_)empty;
authorwenzelm
Sun Dec 28 14:54:38 1997 +0100 (1997-12-28)
changeset 4483caf8ae95c61f
parent 4482 43620c417579
child 4484 220ccae8a590
renamed (is_)null to (is_)empty;
renamed DUPLICATE to DUP;
renamed extend_new to extend;
src/Pure/symtab.ML
     1.1 --- a/src/Pure/symtab.ML	Sat Dec 27 21:49:45 1997 +0100
     1.2 +++ b/src/Pure/symtab.ML	Sun Dec 28 14:54:38 1997 +0100
     1.3 @@ -8,11 +8,11 @@
     1.4  
     1.5  signature SYMTAB =
     1.6  sig
     1.7 -  exception DUPLICATE of string
     1.8 +  exception DUP of string
     1.9    exception DUPS of string list
    1.10    type 'a table
    1.11 -  val null: 'a table
    1.12 -  val is_null: 'a table -> bool
    1.13 +  val empty: 'a table
    1.14 +  val is_empty: 'a table -> bool
    1.15    val lookup: 'a table * string -> 'a option
    1.16    val find_first: (string * 'a -> bool) -> 'a table -> (string * 'a) option
    1.17    val update: (string * 'a) * 'a table -> 'a table
    1.18 @@ -22,8 +22,7 @@
    1.19    val st_of_declist: (string list * 'a) list * 'a table -> 'a table
    1.20    val make: (string * 'a) list -> 'a table
    1.21    val dest: 'a table -> (string * 'a) list
    1.22 -  val extend: ('a * 'a -> bool) -> 'a table * (string * 'a) list -> 'a table
    1.23 -  val extend_new: 'a table * (string * 'a) list -> 'a table
    1.24 +  val extend: 'a table * (string * 'a) list -> 'a table
    1.25    val merge: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table
    1.26    val lookup_multi: 'a list table * string -> 'a list
    1.27    val make_multi: (string * 'a) list -> 'a list table
    1.28 @@ -34,16 +33,16 @@
    1.29  struct
    1.30  
    1.31  (*symbol table errors, such as from update_new*)
    1.32 -exception DUPLICATE of string;
    1.33 +exception DUP of string;
    1.34  exception DUPS of string list;
    1.35  
    1.36  datatype 'a table = Tip | Branch of (string * 'a * 'a table * 'a table);
    1.37  
    1.38  
    1.39 -val null = Tip;
    1.40 +val empty = Tip;
    1.41  
    1.42 -fun is_null Tip = true
    1.43 -  | is_null _ = false;
    1.44 +fun is_empty Tip = true
    1.45 +  | is_empty _ = false;
    1.46  
    1.47  
    1.48  fun lookup (symtab: 'a table, key: string) : 'a option =
    1.49 @@ -81,7 +80,7 @@
    1.50          | upd (Branch(key', entry', left, right)) =
    1.51              if      key < key' then Branch (key', entry', upd left, right)
    1.52              else if key' < key then Branch (key', entry', left, upd right)
    1.53 -            else  raise DUPLICATE(key)
    1.54 +            else  raise DUP(key)
    1.55    in  upd symtab  end;
    1.56  
    1.57  
    1.58 @@ -133,10 +132,10 @@
    1.59      [] => balance (foldr update_new (alst, Tip))
    1.60    | dups => raise DUPS (map fst dups));
    1.61  
    1.62 -fun extend eq (tab, alst) =
    1.63 +fun pre_extend eq (tab, alst) =
    1.64    generic_extend (eq_pair eq) dest make tab alst;
    1.65  
    1.66 -fun extend_new (tab, alst) = extend (K false) (tab, alst);
    1.67 +fun extend (tab, alst) = pre_extend (K false) (tab, alst);
    1.68  
    1.69  fun merge eq (tab1, tab2) =
    1.70    generic_merge (eq_pair eq) dest make tab1 tab2;