Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Binding.str_of;
authorwenzelm
Tue, 03 Mar 2009 15:09:09 +0100
changeset 30219 9224f88c1651
parent 30218 cdd82ba2b4fd
child 30220 11373ba06bf0
Binding.str_of; pretty_name_atts: check Binding.is_empty, not result of Binding.str_of;
src/Pure/Isar/element.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Isar/element.ML	Tue Mar 03 15:09:08 2009 +0100
+++ b/src/Pure/Isar/element.ML	Tue Mar 03 15:09:09 2009 +0100
@@ -125,11 +125,9 @@
         map (fn y => Pretty.block [Pretty.str "  ", Pretty.keyword sep, Pretty.brk 1, y]) ys;
 
 fun pretty_name_atts ctxt (b, atts) sep =
-  let val name = Binding.display b in
-    if name = "" andalso null atts then []
-    else [Pretty.block
-      (Pretty.breaks (Pretty.str name :: Attrib.pretty_attribs ctxt atts @ [Pretty.str sep]))]
-  end;
+  if Binding.is_empty b andalso null atts then []
+  else [Pretty.block (Pretty.breaks
+    (Pretty.str (Binding.str_of b) :: Attrib.pretty_attribs ctxt atts @ [Pretty.str sep]))];
 
 
 (* pretty_stmt *)
isabelle