src/Pure/General/binding.ML

--- a/src/Pure/General/binding.ML	Sat Jan 03 08:36:46 2009 +0100
+++ b/src/Pure/General/binding.ML	Sat Jan 03 08:39:18 2009 +0100
@@ -26,6 +26,8 @@
   val base_name: T -> string
   val pos_of: T -> Position.T
   val dest: T -> (string * bool) list * string
+  val separator: string
+  val is_qualified: string -> bool
   val display: T -> string
 end
 
@@ -39,6 +41,17 @@
 val unique_names = ref true;
 
 
+(** qualification **)
+
+val separator = ".";
+val is_qualified = exists_string (fn s => s = separator);
+
+fun reject_qualified kind s =
+  if is_qualified s then
+    error ("Attempt to declare qualified " ^ kind ^ " " ^ quote s)
+  else s;
+
+
 (** binding representation **)
 
 datatype T = Binding of ((string * bool) list * string) * Position.T;
@@ -54,13 +67,14 @@
 
 fun qualify_base path name =
   if path = "" orelse name = "" then name
-  else path ^ "." ^ name;
+  else path ^ separator ^ name;
 
 val qualify = map_base o qualify_base;
   (*FIXME should all operations on bare names move here from name_space.ML ?*)
 
 fun add_prefix sticky "" b = b
-  | add_prefix sticky prfx b = (map_binding o apfst) (cons (prfx, sticky)) b;
+  | add_prefix sticky prfx b = (map_binding o apfst)
+      (cons ((*reject_qualified "prefix"*) prfx, sticky)) b;
 
 fun map_prefix f (Binding ((prefix, name), pos)) =
   f prefix (name_pos (name, pos));