# HG changeset patch
# User wenzelm
# Date 1236528187 -3600
# Node ID 8ea7a197e2e6415f13dc95343ed1266bee7139a1
# Parent  d4d3fafc9bcaf0f3703767f45fbe48deae8ca0f4
added qualified_name -- emulates old-style qualified bstring;
tuned;

diff -r d4d3fafc9bca -r 8ea7a197e2e6 src/Pure/General/binding.ML
--- a/src/Pure/General/binding.ML	Sun Mar 08 16:53:38 2009 +0100
+++ b/src/Pure/General/binding.ML	Sun Mar 08 17:03:07 2009 +0100
@@ -22,6 +22,7 @@
   val eq_name: binding * binding -> bool
   val empty: binding
   val is_empty: binding -> bool
+  val qualified_name: bstring -> binding
   val qualify: bool -> string -> binding -> binding
   val prefix_of: binding -> (string * bool) list
   val map_prefix: ((string * bool) list -> (string * bool) list) -> binding -> binding
@@ -51,7 +52,7 @@
 
 fun str_of (Binding {prefix, qualifier, name, pos}) =
   let
-    val text = space_implode "." (map #1 qualifier @ [name]);
+    val text = Long_Name.implode (map #1 qualifier @ [name]);
     val props = Position.properties_of pos;
   in Markup.markup (Markup.properties props (Markup.binding name)) text end;
 
@@ -79,6 +80,11 @@
 
 (* user qualifier *)
 
+fun qualified_name "" = empty
+  | qualified_name s =
+      let val (qualifier, name) = split_last (Long_Name.explode s)
+      in make_binding ([], map (rpair false) qualifier, name, Position.none) end;
+
 fun qualify _ "" = I
   | qualify strict qual = map_binding (fn (prefix, qualifier, name, pos) =>
       (prefix, (qual, strict) :: qualifier, name, pos));