# HG changeset patch
# User haftmann
# Date 1226342541 -3600
# Node ID 18ffcbf1b3ae7bc1d04a6209d97ec1d1f75cf86b
# Parent  99492b224b7b9659813737dc8b21e55131868ae6
more verbose element printing

diff -r 99492b224b7b -r 18ffcbf1b3ae src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Mon Nov 10 19:42:20 2008 +0100
+++ b/src/Pure/Isar/element.ML	Mon Nov 10 19:42:21 2008 +0100
@@ -158,8 +158,10 @@
         map (fn y => Pretty.block [Pretty.str "  ", Pretty.keyword sep, Pretty.brk 1, y]) ys;
 
 fun pretty_name_atts ctxt (binding, atts) sep =
-  let val name = Name.name_of binding in
-    if name = "" andalso null atts then []
+  let
+    val name = NameSpace.implode
+      (map fst (Name.prefix_of binding) @ [Name.name_of binding]);
+  in if name = "" andalso null atts then []
     else [Pretty.block
       (Pretty.breaks (Pretty.str name :: Attrib.pretty_attribs ctxt atts @ [Pretty.str sep]))]
   end;