# HG changeset patch
# User wenzelm
# Date 876156099 -7200
# Node ID d5655489867c8f7a83247657793b725dc84eee5b
# Parent  0830d11b8916d0bab12dfdb8ae9ef97d2ad1f937
tuned;

diff -r 0830d11b8916 -r d5655489867c src/Pure/name_space.ML
--- a/src/Pure/name_space.ML	Mon Oct 06 18:41:09 1997 +0200
+++ b/src/Pure/name_space.ML	Mon Oct 06 18:41:39 1997 +0200
@@ -4,9 +4,12 @@
 
 Hierarchically structured name spaces.
 
-More general than ML-like nested structures, but slightly more ad-hoc.
-Does not support absolute addressing.  Unknown short (FIXME?) names
-are implicitely considered to be declared outermost.
+More general than ML-like nested structures, but also slightly more
+ad-hoc.  Does not support absolute addressing.  Unknown names are
+implicitely considered to be declared outermost.
+
+TODO:
+  - absolute paths?
 *)
 
 signature NAME_SPACE =
@@ -14,11 +17,12 @@
   val separator: string		(*single char!*)
   val unpack: string -> string list
   val pack: string list -> string
+  val base: string -> string
   val qualified: string -> bool
   type T
   val dest: T -> string list
   val empty: T
-  val extend: string list -> string list * T -> T
+  val extend: string list * T -> T
   val merge: T * T -> T
   val lookup: T -> string -> string
   val prune: T -> string -> string
@@ -45,6 +49,8 @@
 val unpack = unpack_aux o explode;
 val pack = space_implode separator;
 
+val base = last_elem o unpack;
+
 fun qualified name =
   let val chs = explode name in
     exists (equal separator) chs andalso (length (unpack_aux chs) > 1)
@@ -89,8 +95,8 @@
 
 val empty = make [];
 
-fun extend path (entries, space) =
-  make (map (fn e => path @ unpack e) (rev entries) @ entries_of space);
+fun extend (entries, space) =
+  make (map unpack (rev entries) @ entries_of space);
 
 fun merge (space1, space2) =
   make (merge_lists (entries_of space1) (entries_of space2));
@@ -98,17 +104,18 @@
 
 (* lookup / prune names *)
 
-(* FIXME improve handling of undeclared qualified names (?) *)
 fun lookup space name =
   if_none (Symtab.lookup (tab_of space, name)) name;
 
 fun prune space name =
-  let
-    fun try [] = name
-      | try (nm :: nms) =
-          if lookup space nm = name then nm
-          else try nms;
-  in try (map pack (suffixes1 (unpack name))) end;
+  if not (qualified name) then name
+  else
+    let
+      fun try [] = name
+        | try (nm :: nms) =
+            if lookup space nm = name then nm
+            else try nms;
+    in try (map pack (suffixes1 (unpack name))) end;
 
 
 end;