src/Pure/name_space.ML
changeset 3833 370e845c391f
parent 3803 3e581526ae5e
child 3876 e6f918979f2d
     1.1 --- a/src/Pure/name_space.ML	Fri Oct 10 15:50:46 1997 +0200
     1.2 +++ b/src/Pure/name_space.ML	Fri Oct 10 15:51:14 1997 +0200
     1.3 @@ -7,15 +7,11 @@
     1.4  More general than ML-like nested structures, but also slightly more
     1.5  ad-hoc.  Does not support absolute addressing.  Unknown names are
     1.6  implicitely considered to be declared outermost.
     1.7 -
     1.8 -TODO:
     1.9 -  - absolute paths?
    1.10 -  - also enter into parents!?
    1.11  *)
    1.12  
    1.13  signature NAME_SPACE =
    1.14  sig
    1.15 -  val separator: string		(*single char!*)
    1.16 +  val separator: string         (*single char!*)
    1.17    val unpack: string -> string list
    1.18    val pack: string list -> string
    1.19    val base: string -> string
    1.20 @@ -29,33 +25,19 @@
    1.21    val prune: T -> string -> string
    1.22  end;
    1.23  
    1.24 -structure NameSpace: NAME_SPACE =
    1.25 +structure NameSpace(*: NAME_SPACE FIXME *) =
    1.26  struct
    1.27  
    1.28  
    1.29  (** long identifiers **)
    1.30  
    1.31 -val separator = "'";
    1.32 +val separator = ".";
    1.33  
    1.34 -fun unpack_aux name =
    1.35 -  let
    1.36 -    (*handle trailing separators gracefully*)
    1.37 -    val (chars, seps) = take_suffix (equal separator) name;
    1.38 -    fun expl chs =
    1.39 -      (case take_prefix (not_equal separator) chs of
    1.40 -        (cs, []) => [implode (cs @ seps)]
    1.41 -      | (cs, _ :: cs') => implode cs :: expl cs');
    1.42 -  in expl chars end;
    1.43 -
    1.44 -val unpack = unpack_aux o explode;
    1.45 +val unpack = space_explode separator;
    1.46  val pack = space_implode separator;
    1.47  
    1.48  val base = last_elem o unpack;
    1.49 -
    1.50 -fun qualified name =
    1.51 -  let val chs = explode name in
    1.52 -    exists (equal separator) chs andalso (length (unpack_aux chs) > 1)
    1.53 -  end;
    1.54 +fun qualified name = length (unpack name) > 1;
    1.55  
    1.56  
    1.57  
    1.58 @@ -79,10 +61,16 @@
    1.59  
    1.60  fun make entries =
    1.61    let
    1.62 -    fun accesses entry =
    1.63 -      let val packed = pack entry in
    1.64 -        map (rpair packed o pack) (suffixes1 entry)
    1.65 -      end;
    1.66 +    fun accesses [] = []		(* FIXME !? *)
    1.67 +      | accesses entry =
    1.68 +          let
    1.69 +            val p = pack entry;
    1.70 +            val (q, b) = split_last entry;
    1.71 +            val sfxs = suffixes1 entry;
    1.72 +            val pfxs = map (fn x => x @ [b]) (prefixes1 q);
    1.73 +          in
    1.74 +            map (rpair p o pack) (sfxs @ pfxs)
    1.75 +          end;
    1.76      val mapping = filter_out (op =)
    1.77        (gen_distinct eq_fst (flat (map accesses entries)));
    1.78    in
    1.79 @@ -113,7 +101,7 @@
    1.80    if not (qualified name) then name
    1.81    else
    1.82      let
    1.83 -      fun try [] = name
    1.84 +      fun try [] = "??" ^ separator ^ name      (*hidden name*)
    1.85          | try (nm :: nms) =
    1.86              if lookup space nm = name then nm
    1.87              else try nms;