# HG changeset patch
# User wenzelm
# Date 1237844261 -3600
# Node ID edca392a2abb5a47fcf7d6ff032766019144e1f8
# Parent  2e796219f44104c5ce55661284966a6e686eccb5
pretty_ml/ml_pretty: proper handling of markup and string length;

diff -r 2e796219f441 -r edca392a2abb src/Pure/ML-Systems/polyml-experimental.ML
--- a/src/Pure/ML-Systems/polyml-experimental.ML	Mon Mar 23 21:57:52 2009 +0100
+++ b/src/Pure/ML-Systems/polyml-experimental.ML	Mon Mar 23 22:37:41 2009 +0100
@@ -75,12 +75,30 @@
 
 (* toplevel pretty printing *)
 
-fun pretty_ml (PrettyBlock (ind, _, _, prts)) = ML_Pretty.Block (("", ""), map pretty_ml prts, ind)
-  | pretty_ml (PrettyString s) = ML_Pretty.String (s, size s)
-  | pretty_ml (PrettyBreak (wd, _)) = ML_Pretty.Break (if wd < 99999 then (false, wd) else (true, 2));
+val pretty_ml =
+  let
+    fun convert len (PrettyBlock (ind, _, context, prts)) =
+          let
+            fun property name default =
+              (case List.find (fn ContextProperty (a, _) => name = a | _ => false) context of
+                SOME (ContextProperty (_, b)) => b
+              | NONE => default);
+            val bg = property "begin" "";
+            val en = property "end" "";
+            val len' = property "length" len;
+          in ML_Pretty.Block ((bg, en), map (convert len') prts, ind) end
+      | convert len (PrettyString s) =
+          ML_Pretty.String (s, case Int.fromString len of SOME i => i | NONE => size s)
+      | convert _ (PrettyBreak (wd, _)) =
+          ML_Pretty.Break (if wd < 99999 then (false, wd) else (true, 2));
+  in convert "" end;
 
-fun ml_pretty (ML_Pretty.Block (_, prts, ind)) = PrettyBlock (ind, false, [], map ml_pretty prts)
-  | ml_pretty (ML_Pretty.String (s, _)) = PrettyString s
+fun ml_pretty (ML_Pretty.Block ((bg, en), prts, ind)) =
+      PrettyBlock (ind, false,
+        [ContextProperty ("begin", bg), ContextProperty ("end", en)], map ml_pretty prts)
+  | 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])
   | ml_pretty (ML_Pretty.Break (false, wd)) = PrettyBreak (wd, 0)
   | ml_pretty (ML_Pretty.Break (true, _)) = PrettyBreak (99999, 0);