more verbose element printing
authorhaftmann
Mon Nov 10 19:42:21 2008 +0100 (2008-11-10)
changeset 2873318ffcbf1b3ae
parent 28732 99492b224b7b
child 28734 19277c7a160c
more verbose element printing
src/Pure/Isar/element.ML
     1.1 --- a/src/Pure/Isar/element.ML	Mon Nov 10 19:42:20 2008 +0100
     1.2 +++ b/src/Pure/Isar/element.ML	Mon Nov 10 19:42:21 2008 +0100
     1.3 @@ -158,8 +158,10 @@
     1.4          map (fn y => Pretty.block [Pretty.str "  ", Pretty.keyword sep, Pretty.brk 1, y]) ys;
     1.5  
     1.6  fun pretty_name_atts ctxt (binding, atts) sep =
     1.7 -  let val name = Name.name_of binding in
     1.8 -    if name = "" andalso null atts then []
     1.9 +  let
    1.10 +    val name = NameSpace.implode
    1.11 +      (map fst (Name.prefix_of binding) @ [Name.name_of binding]);
    1.12 +  in if name = "" andalso null atts then []
    1.13      else [Pretty.block
    1.14        (Pretty.breaks (Pretty.str name :: Attrib.pretty_attribs ctxt atts @ [Pretty.str sep]))]
    1.15    end;