# HG changeset patch
# User wenzelm
# Date 1237845447 -3600
# Node ID bcc63fcbc3ce4fd33e81a93b95f7d0eddab9fc2f
# Parent  35d40d961ed284afe4139528f4b44df4826218f3
tuned;

diff -r 35d40d961ed2 -r bcc63fcbc3ce src/Pure/ML-Systems/polyml-experimental.ML
--- 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])