src/Pure/General/name_space.ML
changeset 19030 78d43fe9ac65
parent 19015 1075db658d91
child 19055 4f408867f9d4
     1.1 --- a/src/Pure/General/name_space.ML	Sun Feb 12 21:34:23 2006 +0100
     1.2 +++ b/src/Pure/General/name_space.ML	Sun Feb 12 21:34:24 2006 +0100
     1.3 @@ -127,19 +127,19 @@
     1.4  (* datatype T *)
     1.5  
     1.6  datatype T =
     1.7 -  NameSpace of (string list * string list) Symtab.table;
     1.8 +  NameSpace of ((string list * string list) * stamp) Symtab.table;
     1.9  
    1.10  val empty = NameSpace Symtab.empty;
    1.11  
    1.12  fun lookup (NameSpace tab) xname =
    1.13    (case Symtab.lookup tab xname of
    1.14      NONE => (xname, true)
    1.15 -  | SOME ([], []) => (xname, true)
    1.16 -  | SOME ([name], _) => (name, true)
    1.17 -  | SOME (name :: _, _) => (name, false)
    1.18 -  | SOME ([], name' :: _) => (hidden name', true));
    1.19 +  | SOME (([], []), _) => (xname, true)
    1.20 +  | SOME (([name], _), _) => (name, true)
    1.21 +  | SOME ((name :: _, _), _) => (name, false)
    1.22 +  | SOME (([], name' :: _), _) => (hidden name', true));
    1.23  
    1.24 -fun valid_accesses (NameSpace tab) name = Symtab.fold (fn (xname, (names, _)) =>
    1.25 +fun valid_accesses (NameSpace tab) name = Symtab.fold (fn (xname, ((names, _), _)) =>
    1.26    if not (null names) andalso hd names = name then cons xname else I) tab [];
    1.27  
    1.28  
    1.29 @@ -169,7 +169,11 @@
    1.30  (* basic operations *)
    1.31  
    1.32  fun map_space f xname (NameSpace tab) =
    1.33 -  NameSpace (Symtab.update (xname, f (the_default ([], []) (Symtab.lookup tab xname))) tab);
    1.34 +  let val entry' =
    1.35 +    (case Symtab.lookup tab xname of
    1.36 +      NONE => f ([], [])
    1.37 +    | SOME (entry, _) => f entry)
    1.38 +  in NameSpace (Symtab.update (xname, (entry', stamp ())) tab) end;
    1.39  
    1.40  fun del (name: string) = remove (op =) name;
    1.41  fun add name names = name :: del name names;
    1.42 @@ -196,9 +200,13 @@
    1.43  
    1.44  (* merge *)
    1.45  
    1.46 -fun merge (NameSpace tab1, space2) = Symtab.fold (fn (xname, (names1, names1')) =>
    1.47 -  xname |> map_space (fn (names2, names2') =>
    1.48 -    (Library.merge (op =) (names2, names1), Library.merge (op =) (names2', names1')))) tab1 space2;
    1.49 +fun merge (NameSpace tab1, NameSpace tab2) =
    1.50 +  NameSpace ((tab1, tab2) |> Symtab.join
    1.51 +    (K (fn (((names1, names1'), stamp1), ((names2, names2'), stamp2)) =>
    1.52 +      if stamp1 = stamp2 then raise Symtab.SAME
    1.53 +      else
    1.54 +        ((Library.merge (op =) (names2, names1),
    1.55 +          Library.merge (op =) (names2', names1')), stamp ()))));
    1.56  
    1.57  
    1.58