# HG changeset patch
# User wenzelm
# Date 1450701585 -3600
# Node ID c0f34fe6aa613a62981843914ef59bad3165cfdb
# Parent  e4f9d8f094fe9248147481d063cc07dc04e5905a
clarified length of block with pre-existant forced breaks;

diff -r e4f9d8f094fe -r c0f34fe6aa61 src/Pure/General/pretty.ML
--- a/src/Pure/General/pretty.ML	Sun Dec 20 13:56:02 2015 +0100
+++ b/src/Pure/General/pretty.ML	Mon Dec 21 13:39:45 2015 +0100
@@ -118,11 +118,22 @@
   | length (Break (_, wd, _)) = wd
   | length (Str (_, len)) = len;
 
-fun body_length [] len = len
-  | body_length (e :: es) len = body_length es (length e + len);
+fun make_block markup consistent indent body =
+  let
+    fun body_length prts len =
+      let
+        val (line, rest) = take_prefix (fn Break (true, _, _) => false | _ => true) prts;
+        val len' = Int.max (fold (Integer.add o length) line 0, len);
+      in
+        (case rest of
+          Break (true, _, ind) :: rest' =>
+            body_length (Break (false, indent + ind, 0) :: rest') len'
+        | [] => len')
+      end;
+  in Block (markup, consistent, indent, body, body_length body 0) end;
 
-fun make_block m consistent indent es = Block (m, consistent, indent, es, body_length es 0);
-fun markup_block m indent es = make_block (Markup.output m) false indent es;
+fun markup_block markup indent es =
+  make_block (Markup.output markup) false indent es;
 
 
 
diff -r e4f9d8f094fe -r c0f34fe6aa61 src/Pure/General/pretty.scala
--- a/src/Pure/General/pretty.scala	Sun Dec 20 13:56:02 2015 +0100
+++ b/src/Pure/General/pretty.scala	Mon Dec 21 13:39:45 2015 +0100
@@ -63,7 +63,20 @@
       consistent: Boolean,
       indent: Int,
       body: List[Tree]): Tree =
-    Block(markup, consistent, indent, body, (0.0 /: body) { case (n, t) => n + t.length })
+  {
+    def body_length(prts: List[Tree], len: Double): Double =
+    {
+      val (line, rest) =
+        Library.take_prefix[Tree]({ case Break(true, _, _) => false case _ => true }, prts)
+      val len1 = ((0.0 /: line) { case (l, t) => l + t.length }) max len
+      rest match {
+        case Break(true, _, ind) :: rest1 =>
+          body_length(Break(false, indent + ind, 0) :: rest1, len1)
+        case Nil => len1
+      }
+    }
+    Block(markup, consistent, indent, body, body_length(body, 0.0))
+  }
 
 
   /* formatted output */
diff -r e4f9d8f094fe -r c0f34fe6aa61 src/Pure/library.scala
--- a/src/Pure/library.scala	Sun Dec 20 13:56:02 2015 +0100
+++ b/src/Pure/library.scala	Mon Dec 21 13:39:45 2015 +0100
@@ -205,7 +205,10 @@
     try { Some(new Regex(s)) } catch { case ERROR(_) => None }
 
 
-  /* canonical list operations */
+  /* lists */
+
+  def take_prefix[A](pred: A => Boolean, xs: List[A]): (List[A], List[A]) =
+    (xs.takeWhile(pred), xs.dropWhile(pred))
 
   def member[A, B](xs: List[A])(x: B): Boolean = xs.contains(x)
   def insert[A](x: A)(xs: List[A]): List[A] = if (xs.contains(x)) xs else x :: xs