more verbose element printing
authorhaftmann
Mon, 10 Nov 2008 19:42:21 +0100
changeset 28733 18ffcbf1b3ae
parent 28732 99492b224b7b
child 28734 19277c7a160c
more verbose element printing
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;