# HG changeset patch
# User wenzelm
# Date 1459626891 -7200
# Node ID 5c678ee5d34a5e6624111c76b175960f6a277936
# Parent  d3ff367a16a0168da59de43bcc2957789fa8a640
proper type;
tuned;

diff -r d3ff367a16a0 -r 5c678ee5d34a src/Pure/General/pretty.ML
--- 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;
diff -r d3ff367a16a0 -r 5c678ee5d34a src/Pure/General/pretty.scala
--- 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)