src/Pure/General/name_space.ML
changeset 26440 feeb83f9657f
parent 25225 e638164593bf
child 26657 35249f5367b3
     1.1 --- a/src/Pure/General/name_space.ML	Thu Mar 27 17:35:56 2008 +0100
     1.2 +++ b/src/Pure/General/name_space.ML	Thu Mar 27 17:35:57 2008 +0100
     1.3 @@ -6,8 +6,8 @@
     1.4  are considered global; no support for absolute addressing.
     1.5  *)
     1.6  
     1.7 -type bstring = string;    (*names to be bound / internalized*)
     1.8 -type xstring = string;    (*externalized names / to be printed*)
     1.9 +type bstring = string;    (*names to be bound*)
    1.10 +type xstring = string;    (*external names*)
    1.11  
    1.12  signature BASIC_NAME_SPACE =
    1.13  sig
    1.14 @@ -157,14 +157,14 @@
    1.15    let
    1.16      fun valid unique xname =
    1.17        let val (name', uniq) = lookup space xname
    1.18 -      in name = name' andalso (uniq orelse (not unique)) end;
    1.19 +      in name = name' andalso (uniq orelse not unique) end;
    1.20  
    1.21 -    fun ex [] = if valid false name then name else hidden name
    1.22 -      | ex (nm :: nms) = if valid (! unique_names) nm then nm else ex nms;
    1.23 +    fun ext [] = if valid false name then name else hidden name
    1.24 +      | ext (nm :: nms) = if valid (! unique_names) nm then nm else ext nms;
    1.25    in
    1.26      if ! long_names then name
    1.27      else if ! short_names then base name
    1.28 -    else ex (get_accesses space name)
    1.29 +    else ext (get_accesses space name)
    1.30    end;
    1.31  
    1.32  
    1.33 @@ -176,14 +176,11 @@
    1.34    NameSpace (Symtab.map_default (xname, (([], []), stamp ()))
    1.35      (fn (entry, _) => (f entry, stamp ())) tab, xtab);
    1.36  
    1.37 -fun del (name: string) = remove (op =) name;
    1.38 -fun add name names = name :: del name names;
    1.39 -
    1.40  in
    1.41  
    1.42 -val del_name = map_space o apfst o del;
    1.43 -val add_name = map_space o apfst o add;
    1.44 -val add_name' = map_space o apsnd o add;
    1.45 +val del_name = map_space o apfst o remove (op =);
    1.46 +val add_name = map_space o apfst o update (op =);
    1.47 +val add_name' = map_space o apsnd o update (op =);
    1.48  
    1.49  end;
    1.50  
    1.51 @@ -222,6 +219,7 @@
    1.52    in NameSpace (tab', xtab') end;
    1.53  
    1.54  
    1.55 +
    1.56  (** naming contexts **)
    1.57  
    1.58  (* datatype naming *)