src/Pure/General/name_space.ML
changeset 15570 8d8c70b41bab
parent 15531 08c8dad8e399
child 15574 b1d1b5bfc464
     1.1 --- a/src/Pure/General/name_space.ML	Thu Mar 03 09:22:35 2005 +0100
     1.2 +++ b/src/Pure/General/name_space.ML	Thu Mar 03 12:43:01 2005 +0100
     1.3 @@ -50,7 +50,7 @@
     1.4  val unpack = space_explode separator;
     1.5  val pack = space_implode separator;
     1.6  
     1.7 -val base = last_elem o unpack;
     1.8 +val base = List.last o unpack;
     1.9  
    1.10  fun map_base f name =
    1.11    let val uname = unpack name
    1.12 @@ -75,7 +75,7 @@
    1.13  (* basic operations *)
    1.14  
    1.15  fun map_space f xname tab =
    1.16 -  Symtab.update ((xname, f (if_none (Symtab.lookup (tab, xname)) ([], []))), tab);
    1.17 +  Symtab.update ((xname, f (getOpt (Symtab.lookup (tab, xname), ([], [])))), tab);
    1.18  
    1.19  fun change f xname (name, tab) =
    1.20    map_space (fn (names, names') => (f names name, names')) xname tab;
    1.21 @@ -100,9 +100,9 @@
    1.22  fun extend_aux (name, tab) =
    1.23    if is_hidden name then
    1.24      error ("Attempt to declare hidden name " ^ quote name)
    1.25 -  else foldl (fn (tb, xname) => change add xname (name, tb)) (tab, accesses name);
    1.26 +  else Library.foldl (fn (tb, xname) => change add xname (name, tb)) (tab, accesses name);
    1.27  
    1.28 -fun extend (NameSpace tab, names) = NameSpace (foldr extend_aux (names, tab));
    1.29 +fun extend (NameSpace tab, names) = NameSpace (Library.foldr extend_aux (names, tab));
    1.30  
    1.31  
    1.32  (* merge *)             (*1st preferred over 2nd*)
    1.33 @@ -123,10 +123,10 @@
    1.34    else if is_hidden name then
    1.35      error ("Attempt to hide hidden name " ^ quote name)
    1.36    else (change' add name (name,
    1.37 -    foldl (fn (tb, xname) => change del xname (name, tb))
    1.38 +    Library.foldl (fn (tb, xname) => change del xname (name, tb))
    1.39        (tab, if fully then accesses name else [base name])));
    1.40  
    1.41 -fun hide fully (NameSpace tab, names) = NameSpace (foldr (hide_aux fully) (names, tab));
    1.42 +fun hide fully (NameSpace tab, names) = NameSpace (Library.foldr (hide_aux fully) (names, tab));
    1.43  
    1.44  
    1.45  (* intern / extern names *)
    1.46 @@ -175,7 +175,7 @@
    1.47  
    1.48  fun dest (NameSpace tab) =
    1.49    map (apsnd (sort (int_ord o pairself size)))
    1.50 -    (Symtab.dest (Symtab.make_multi (mapfilter dest_entry (Symtab.dest tab))));
    1.51 +    (Symtab.dest (Symtab.make_multi (List.mapPartial dest_entry (Symtab.dest tab))));
    1.52  
    1.53  
    1.54  end;