# HG changeset patch
# User wenzelm
# Date 1309007338 -7200
# Node ID 6629e2dedb009ce554e927a03fcfcf6e97ce89e9
# Parent  1cf2256f1b077e02af86a2167a58d2a2853af34d
clarified Binding.str_of/print: show full prefix + qualifier, which is relevant for print_locale, for example;
discontinued unused Binding.qualified_name_of;

diff -r 1cf2256f1b07 -r 6629e2dedb00 src/Pure/General/binding.ML
--- a/src/Pure/General/binding.ML	Sat Jun 25 15:02:12 2011 +0200
+++ b/src/Pure/General/binding.ML	Sat Jun 25 15:08:58 2011 +0200
@@ -24,7 +24,6 @@
   val qualify: bool -> string -> binding -> binding
   val qualified: bool -> string -> binding -> binding
   val qualified_name: string -> binding
-  val qualified_name_of: binding -> string
   val prefix_of: binding -> (string * bool) list
   val map_prefix: ((string * bool) list -> (string * bool) list) -> binding -> binding
   val prefix: bool -> string -> binding -> binding
@@ -100,10 +99,6 @@
       let val (qualifier, name) = split_last (Long_Name.explode s)
       in make_binding (false, [], map (rpair false) qualifier, name, Position.none) end;
 
-fun qualified_name_of (b as Binding {qualifier, name, ...}) =
-  if is_empty b then ""
-  else Long_Name.implode (map #1 qualifier @ [name]);
-
 
 (* system prefix *)
 
@@ -126,9 +121,11 @@
 
 (* print *)
 
-fun str_of binding =
-  qualified_name_of binding
-  |> Markup.markup (Position.markup (pos_of binding) (Markup.binding (name_of binding)));
+fun str_of (Binding {prefix, qualifier, name, pos, ...}) =
+  if name = "" then ""
+  else
+    Long_Name.implode (map #1 (prefix @ qualifier) @ [name])
+    |> Markup.markup (Position.markup pos (Markup.binding name));
 
 val print = quote o str_of;