moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
moved separator/is_qualified from binding.ML back to name_space.ML -- only name space introduces an explicit notation for qualified names;
type binding: maintain explicit qualifier, indepently of base name;
tuned signature of Binding: renamed name_pos to make, renamed base_name to name_of, renamed map_base to map_name, added mandatory flag to qualify, simplified map_prefix (formerly unused);
Binding.str_of: include markup with position properties;
misc tuning;

--- a/src/Pure/General/binding.ML	Tue Mar 03 17:42:30 2009 +0100
+++ b/src/Pure/General/binding.ML	Tue Mar 03 18:31:59 2009 +0100
@@ -5,77 +5,93 @@
 Structured name bindings.
 *)
 
+type bstring = string;    (*primitive names to be bound*)
+
 signature BINDING =
 sig
-  val separator: string
-  val is_qualified: string -> bool
   type binding
+  val dest: binding -> (string * bool) list * (string * bool) list * bstring
   val str_of: binding -> string
-  val name_pos: string * Position.T -> binding
-  val name: string -> binding
+  val make: bstring * Position.T -> binding
+  val name: bstring -> binding
+  val pos_of: binding -> Position.T
+  val name_of: binding -> string
+  val map_name: (bstring -> bstring) -> binding -> binding
   val empty: binding
-  val map_base: (string -> string) -> binding -> binding
-  val qualify: string -> binding -> binding
+  val is_empty: binding -> bool
+  val qualify: bool -> string -> binding -> binding
+  val map_prefix: ((string * bool) list -> (string * bool) list) -> binding -> binding
   val add_prefix: bool -> string -> binding -> binding
-  val map_prefix: ((string * bool) list -> binding -> binding) -> binding -> binding
-  val is_empty: binding -> bool
-  val base_name: binding -> string
-  val pos_of: binding -> Position.T
-  val dest: binding -> (string * bool) list * string
 end;
 
 structure Binding: BINDING =
 struct
 
-(** qualification **)
-
-val separator = ".";
-val is_qualified = exists_string (fn s => s = separator);
+(** representation **)
 
-fun reject_qualified kind s =
-  if is_qualified s then
-    error ("Attempt to declare qualified " ^ kind ^ " " ^ quote s)
-  else s;
+(* datatype *)
 
+type component = string * bool;   (*name with mandatory flag*)
 
-(** binding representation **)
-
-datatype binding = Binding of ((string * bool) list * string) * Position.T;
-  (* (prefix components (with mandatory flag), base name, position) *)
+datatype binding = Binding of
+ {prefix: component list,         (*system prefix*)
+  qualifier: component list,      (*user qualifier*)
+  name: bstring,                  (*base name*)
+  pos: Position.T};               (*source position*)
 
-fun str_of (Binding ((prefix, name), _)) =
-  let
-    fun mk_prefix (prfx, true) = prfx
-      | mk_prefix (prfx, false) = enclose "(" ")" prfx
-  in space_implode "." (map mk_prefix prefix) ^ ":" ^ name end;
+fun make_binding (prefix, qualifier, name, pos) =
+  Binding {prefix = prefix, qualifier = qualifier, name = name, pos = pos};
+
+fun map_binding f (Binding {prefix, qualifier, name, pos}) =
+  make_binding (f (prefix, qualifier, name, pos));
+
+fun dest (Binding {prefix, qualifier, name, ...}) = (prefix, qualifier, name);
 
 
-fun name_pos (name, pos) = Binding (([], name), pos);
-fun name name = name_pos (name, Position.none);
-val empty = name "";
+(* diagnostic output *)
 
-fun map_binding f (Binding (prefix_name, pos)) = Binding (f prefix_name, pos);
+val str_of_components = implode o map (fn (s, true) => s ^ "!" | (s, false) => s ^ "?");
 
-val map_base = map_binding o apsnd;
+fun str_of (Binding {prefix, qualifier, name, pos}) =
+  let
+    val text =
+      (if null prefix then "" else enclose "(" ")" (str_of_components prefix)) ^
+      str_of_components qualifier ^ ":" ^ name;
+    val props = Position.properties_of pos;
+  in Markup.markup (Markup.properties props (Markup.binding name)) text end;
 
-fun qualify_base path name =
-  if path = "" orelse name = "" then name
-  else path ^ separator ^ name;
+
+
+(** basic operations **)
+
+(* name and position *)
+
+fun make (name, pos) = make_binding ([], [], name, pos);
+fun name name = make (name, Position.none);
 
-val qualify = map_base o qualify_base;
-  (*FIXME should all operations on bare names move here from name_space.ML ?*)
+fun pos_of (Binding {pos, ...}) = pos;
+fun name_of (Binding {name, ...}) = name;
+
+fun map_name f = map_binding (fn (prefix, qualifier, name, pos) => (prefix, qualifier, f name, pos));
 
-fun add_prefix sticky "" b = b
-  | add_prefix sticky prfx b = (map_binding o apfst)
-      (cons ((*reject_qualified "prefix"*) prfx, sticky)) b;
+val empty = name "";
+fun is_empty b = name_of b = "";
+
+
+(* user qualifier *)
 
-fun map_prefix f (Binding ((prefix, name), pos)) =
-  f prefix (name_pos (name, pos));
+fun qualify _ "" = I
+  | qualify mandatory qual = map_binding (fn (prefix, qualifier, name, pos) =>
+      (prefix, (qual, mandatory) :: qualifier, name, pos));
+
 
-fun is_empty (Binding ((_, name), _)) = name = "";
-fun base_name (Binding ((_, name), _)) = name;
-fun pos_of (Binding (_, pos)) = pos;
-fun dest (Binding (prefix_name, _)) = prefix_name;
+(* system prefix *)
+
+fun map_prefix f = map_binding (fn (prefix, qualifier, name, pos) =>
+  (f prefix, qualifier, name, pos));
+
+fun add_prefix _ "" = I
+  | add_prefix mandatory prfx = map_prefix (cons (prfx, mandatory));
 
 end;
 

--- a/src/Pure/General/name_space.ML	Tue Mar 03 17:42:30 2009 +0100
+++ b/src/Pure/General/name_space.ML	Tue Mar 03 18:31:59 2009 +0100
@@ -6,7 +6,6 @@
 Cf. Pure/General/binding.ML
 *)
 
-type bstring = string;    (*simple names to be bound -- legacy*)
 type xstring = string;    (*external names*)
 
 signature BASIC_NAME_SPACE =
@@ -67,8 +66,8 @@
 fun hidden name = "??." ^ name;
 val is_hidden = String.isPrefix "??.";
 
-val separator = Binding.separator;
-val is_qualified = Binding.is_qualified;
+val separator = ".";
+val is_qualified = exists_string (fn s => s = separator);
 
 val implode_name = space_implode separator;
 val explode_name = space_explode separator;
@@ -295,13 +294,13 @@
     in space |> fold (add_name name) accs |> put_accesses name accs' end;
 
 fun full_name naming b =
-  let val (prefix, bname) = Binding.dest b
-  in full_internal (apply_prefix prefix naming) bname end;
+  let val (prefix, qualifier, bname) = Binding.dest b
+  in full_internal (apply_prefix (prefix @ qualifier) naming) bname end;
 
 fun declare bnaming b =
   let
-    val (prefix, bname) = Binding.dest b;
-    val naming = apply_prefix prefix bnaming;
+    val (prefix, qualifier, bname) = Binding.dest b;
+    val naming = apply_prefix (prefix @ qualifier) bnaming;
     val name = full_internal naming bname;
   in declare_internal naming name #> pair name end;