--- 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