# HG changeset patch
# User wenzelm
# Date 1364479227 -3600
# Node ID 4e084727faaedf6f6665bc8c9c4d2d1b209942af
# Parent  cdb4b7dc76cbec4caa602a55d12b207ec9c62926
maintain integer indentation during formatting -- it needs to be implemented by repeated spaces eventually;
always round block indentation upwards, to ensure that text moves visually to the right of the "hanging" part;

diff -r cdb4b7dc76cb -r 4e084727faae src/Pure/General/pretty.scala
--- a/src/Pure/General/pretty.scala	Thu Mar 28 14:47:37 2013 +0100
+++ b/src/Pure/General/pretty.scala	Thu Mar 28 15:00:27 2013 +0100
@@ -101,7 +101,7 @@
     }
 
     val breakgain = margin / 20
-    val emergencypos = margin / 2
+    val emergencypos = (margin / 2).round.toInt
 
     def content_length(tree: XML.Tree): Double =
       XML.traverse_text(List(tree))(0.0)(_ + metric(_))
@@ -122,12 +122,12 @@
         case t :: ts => t :: forcenext(ts)
       }
 
-    def format(trees: XML.Body, blockin: Double, after: Double, text: Text): Text =
+    def format(trees: XML.Body, blockin: Int, after: Double, text: Text): Text =
       trees match {
         case Nil => text
 
         case Block(indent, body) :: ts =>
-          val pos1 = text.pos + indent
+          val pos1 = (text.pos + indent).ceil.toInt
           val pos2 = pos1 % emergencypos
           val blockin1 =
             if (pos1 < emergencypos) pos1
@@ -139,8 +139,8 @@
         case Break(wd) :: ts =>
           if (text.pos + wd <= ((margin - breakdist(ts, after)) max (blockin + breakgain)))
             format(ts, blockin, after, text.blanks(wd))
-          else format(ts, blockin, after, text.newline.blanks(blockin.toInt))
-        case FBreak :: ts => format(ts, blockin, after, text.newline.blanks(blockin.toInt))
+          else format(ts, blockin, after, text.newline.blanks(blockin))
+        case FBreak :: ts => format(ts, blockin, after, text.newline.blanks(blockin))
 
         case XML.Wrapped_Elem(markup, body1, body2) :: ts =>
           val btext = format(body2, blockin, breakdist(ts, after), text.copy(tx = Nil))
@@ -157,7 +157,7 @@
         case XML.Text(s) :: ts => format(ts, blockin, after, text.string(s))
       }
 
-    format(standard_format(input), 0.0, 0.0, Text()).content
+    format(standard_format(input), 0, 0.0, Text()).content
   }
 
   def string_of(input: XML.Body, margin: Double = margin_default,