# HG changeset patch
# User haftmann
# Date 1226582347 -3600
# Node ID 8cbb7cfcfb5b53cc0898ed91f650824d926e48f6
# Parent  b1fd60fee6524c894e8745062fd12094025e8026
diagnostic output for name bindings

diff -r b1fd60fee652 -r 8cbb7cfcfb5b src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Thu Nov 13 01:31:20 2008 +0100
+++ b/src/Pure/Isar/element.ML	Thu Nov 13 14:19:07 2008 +0100
@@ -159,8 +159,7 @@
 
 fun pretty_name_atts ctxt (binding, atts) sep =
   let
-    val name = NameSpace.implode
-      (map fst (Name.prefix_of binding) @ [Name.name_of binding]);
+    val name = Name.output binding;
   in if name = "" andalso null atts then []
     else [Pretty.block
       (Pretty.breaks (Pretty.str name :: Attrib.pretty_attribs ctxt atts @ [Pretty.str sep]))]
diff -r b1fd60fee652 -r 8cbb7cfcfb5b src/Pure/name.ML
--- a/src/Pure/name.ML	Thu Nov 13 01:31:20 2008 +0100
+++ b/src/Pure/name.ML	Thu Nov 13 14:19:07 2008 +0100
@@ -38,6 +38,7 @@
   val add_prefix: bool -> string -> binding -> binding
   val map_name: (string -> string) -> binding -> binding
   val qualified: string -> binding -> binding
+  val output: binding -> string
 end;
 
 structure Name: NAME =
@@ -171,4 +172,8 @@
 val map_name = map_binding o apfst o apsnd;
 val qualified = map_name o NameSpace.qualified;
 
+fun output (Binding ((prefix, name), _)) =
+  if null prefix orelse name = "" then name
+  else NameSpace.implode (map fst prefix) ^ " / " ^ name;
+
 end;