# HG changeset patch
# User wenzelm
# Date 1365430014 -7200
# Node ID 1275716f395b9bbf450861044c945de1c04e65a6
# Parent  ff2d241dcde13df4f5ee5694102f99fdcbb3d19b
more defensive representation of forced break within PolyML.PrettyBreak -- avoid accidental blowup if low-level operations are used, notably PolyML.makestring or its variant General.exnMessage;

diff -r ff2d241dcde1 -r 1275716f395b src/Pure/ML-Systems/polyml.ML
--- a/src/Pure/ML-Systems/polyml.ML	Mon Apr 08 15:44:09 2013 +0200
+++ b/src/Pure/ML-Systems/polyml.ML	Mon Apr 08 16:06:54 2013 +0200
@@ -120,7 +120,11 @@
 
 val pretty_ml =
   let
-    fun convert len (PolyML.PrettyBlock (ind, _, context, prts)) =
+    fun convert _ (PolyML.PrettyBreak (wd, _)) = ML_Pretty.Break (false, wd)
+      | convert _ (PolyML.PrettyBlock (ind, _,
+            [PolyML.ContextProperty ("fbrk", _)], [PolyML.PrettyString " "])) =
+          ML_Pretty.Break (true, 1)
+      | convert len (PolyML.PrettyBlock (ind, _, context, prts)) =
           let
             fun property name default =
               (case List.find (fn PolyML.ContextProperty (a, _) => name = a | _ => false) context of
@@ -132,11 +136,13 @@
           in ML_Pretty.Block ((bg, en), map (convert len') prts, ind) end
       | convert len (PolyML.PrettyString s) =
           ML_Pretty.String (s, case Int.fromString len of SOME i => i | NONE => size s)
-      | convert _ (PolyML.PrettyBreak (wd, _)) =
-          ML_Pretty.Break (if wd < 99999 then (false, wd) else (true, 2));
   in convert "" end;
 
-fun ml_pretty (ML_Pretty.Block ((bg, en), prts, ind)) =
+fun ml_pretty (ML_Pretty.Break (false, wd)) = PolyML.PrettyBreak (wd, 0)
+  | ml_pretty (ML_Pretty.Break (true, _)) =
+      PolyML.PrettyBlock (0, false, [PolyML.ContextProperty ("fbrk", "")],
+        [PolyML.PrettyString " "])
+  | ml_pretty (ML_Pretty.Block ((bg, en), prts, ind)) =
       let val context =
         (if bg = "" then [] else [PolyML.ContextProperty ("begin", bg)]) @
         (if en = "" then [] else [PolyML.ContextProperty ("end", en)])
@@ -144,9 +150,7 @@
   | ml_pretty (ML_Pretty.String (s, len)) =
       if len = size s then PolyML.PrettyString s
       else PolyML.PrettyBlock
-        (0, false, [PolyML.ContextProperty ("length", Int.toString len)], [PolyML.PrettyString s])
-  | ml_pretty (ML_Pretty.Break (false, wd)) = PolyML.PrettyBreak (wd, 0)
-  | ml_pretty (ML_Pretty.Break (true, _)) = PolyML.PrettyBreak (99999, 0);
+        (0, false, [PolyML.ContextProperty ("length", Int.toString len)], [PolyML.PrettyString s]);
 
 fun toplevel_pp context (_: string list) pp =
   use_text context (1, "pp") false