--- a/src/Pure/General/pretty.ML Sat Apr 02 21:10:07 2016 +0200
+++ b/src/Pure/General/pretty.ML Sat Apr 02 21:54:51 2016 +0200
@@ -395,7 +395,7 @@
(map from_ML prts)
| from_ML (ML_Pretty.Break (force, wd, ind)) =
Break (force, FixedInt.toInt wd, FixedInt.toInt ind)
- | from_ML (ML_Pretty.String (s, len)) = Str (s, FixedInt.toInt (force_nat len));
+ | from_ML (ML_Pretty.String (s, len)) = Str (s, force_nat (FixedInt.toInt len));
val to_polyml = to_ML ~1 #> ML_Pretty.to_polyml;
val from_polyml = ML_Pretty.from_polyml #> from_ML;
--- a/src/Pure/General/pretty.scala Sat Apr 02 21:10:07 2016 +0200
+++ b/src/Pure/General/pretty.scala Sat Apr 02 21:54:51 2016 +0200
@@ -48,6 +48,8 @@
/* markup trees with physical blocks and breaks */
+ private def force_nat(i: Int): Int = i max 0
+
private sealed abstract class Tree { def length: Double }
private case class Block(
markup: Option[(Markup, Option[XML.Body])],
@@ -83,8 +85,6 @@
/* formatted output */
- private def force_nat(i: Int): Int = i max 0
-
private sealed case class Text(tx: XML.Body = Nil, pos: Double = 0.0, nl: Int = 0)
{
def newline: Text = copy(tx = fbrk :: tx, pos = 0.0, nl = nl + 1)