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;
authorwenzelm
Mon, 23 Mar 2009 22:57:27 +0100
changeset 30679 bcc63fcbc3ce
parent 30678 35d40d961ed2
child 30680 0863bb353065
tuned;
src/Pure/ML-Systems/polyml-experimental.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/ML-Systems/polyml-experimental.ML	Mon Mar 23 22:56:03 2009 +0100
+++ b/src/Pure/ML-Systems/polyml-experimental.ML	Mon Mar 23 22:57:27 2009 +0100
@@ -94,8 +94,10 @@
   in convert "" end;
 
 fun ml_pretty (ML_Pretty.Block ((bg, en), prts, ind)) =
-      PrettyBlock (ind, false,
-        [ContextProperty ("begin", bg), ContextProperty ("end", en)], map ml_pretty prts)
+      let val context =
+        (if bg = "" then [] else [ContextProperty ("begin", bg)]) @
+        (if en = "" then [] else [ContextProperty ("end", en)])
+      in PrettyBlock (ind, false, context, map ml_pretty prts) end
   | ml_pretty (ML_Pretty.String (s, len)) =
       if len = size s then PrettyString s
       else PrettyBlock (0, false, [ContextProperty ("length", Int.toString len)], [PrettyString s])
isabelle