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.
tuned output;
authorwenzelm
Sun, 03 May 2015 17:36:46 +0200
changeset 60243 5901cb4db0ae
parent 60242 3a8501876dba
child 60244 523ec7e4b022
tuned output;
src/Pure/Isar/attrib.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Isar/attrib.ML	Sun May 03 17:19:27 2015 +0200
+++ b/src/Pure/Isar/attrib.ML	Sun May 03 17:36:46 2015 +0200
@@ -160,11 +160,13 @@
   | pretty_attribs ctxt srcs = [Pretty.enum "," "[" "]" (map (Token.pretty_src ctxt) srcs)];
 
 fun pretty_binding ctxt (b, atts) sep =
-  if is_empty_binding (b, atts) then []
-  else if Binding.is_empty b then
-    [Pretty.block (pretty_attribs ctxt atts @ [Pretty.str sep])]
-  else
-    [Pretty.block (Binding.pretty b :: Pretty.brk 1 :: pretty_attribs ctxt atts @ [Pretty.str sep])];
+  (case (Binding.is_empty b, null atts) of
+    (true, true) => []
+  | (false, true) => [Pretty.block [Binding.pretty b, Pretty.str sep]]
+  | (true, false) => [Pretty.block (pretty_attribs ctxt atts @ [Pretty.str sep])]
+  | (false, false) =>
+      [Pretty.block
+        (Binding.pretty b :: Pretty.brk 1 :: pretty_attribs ctxt atts @ [Pretty.str sep])]);
 
 
 (* get attributes *)
isabelle