# HG changeset patch
# User wenzelm
# Date 1273180041 -7200
# Node ID 58020b59baf7f262a8ea90a2b2c3be954f476f79
# Parent  b1956bc8f5857b9be5b319904eb5a177f9fc4cdb
basic formatting of pretty trees;
line-up ML vs. Scala sources;

diff -r b1956bc8f585 -r 58020b59baf7 src/Pure/General/pretty.ML
--- a/src/Pure/General/pretty.ML	Thu May 06 22:54:25 2010 +0200
+++ b/src/Pure/General/pretty.ML	Thu May 06 23:07:21 2010 +0200
@@ -249,9 +249,9 @@
 
 (*Add the lengths of the expressions until the next Break; if no Break then
   include "after", to account for text following this block.*)
-fun breakdist (Block (_, _, _, len) :: es, after) = len + breakdist (es, after)
+fun breakdist (Break _ :: _, _) = 0
+  | breakdist (Block (_, _, _, len) :: es, after) = len + breakdist (es, after)
   | breakdist (String (_, len) :: es, after) = len + breakdist (es, after)
-  | breakdist (Break _ :: _, _) = 0
   | breakdist ([], after) = after;
 
 (*Search for the next break (at this or higher levels) and force it to occur.*)
@@ -280,7 +280,6 @@
             (*if this block was broken then force the next break*)
             val es' = if nl < #nl btext then forcenext es else es;
           in format (es', block, after) btext end
-      | String str => format (es, block, after) (string str text)
       | Break (force, wd) =>
           let val {margin, breakgain, ...} = ! margin_info in
             (*no break if text to next break fits on this line
@@ -290,7 +289,8 @@
                   pos + wd <= Int.max (margin - breakdist (es, after), blockin + breakgain)
                 then text |> blanks wd  (*just insert wd blanks*)
                 else text |> newline |> indentation block)
-          end);
+          end
+      | String str => format (es, block, after) (string str text));
 
 in
 
diff -r b1956bc8f585 -r 58020b59baf7 src/Pure/General/pretty.scala
--- a/src/Pure/General/pretty.scala	Thu May 06 22:54:25 2010 +0200
+++ b/src/Pure/General/pretty.scala	Thu May 06 23:07:21 2010 +0200
@@ -1,7 +1,7 @@
 /*  Title:      Pure/General/pretty.scala
     Author:     Makarius
 
-Symbolic pretty printing.
+Generic pretty printing module.
 */
 
 package isabelle
@@ -9,6 +9,8 @@
 
 object Pretty
 {
+  /* markup trees with physical blocks and breaks */
+
   object Block
   {
     def apply(indent: Int, body: List[XML.Tree]): XML.Tree =
@@ -47,4 +49,64 @@
         case _ => false
       }
   }
+
+
+  /* formatted output */
+
+  private case class Text(tx: List[String] = Nil, val pos: Int = 0, val nl: Int = 0)
+  {
+    def newline: Text = copy(tx = "\n" :: tx, pos = 0, nl = nl + 1)
+    def string(s: String): Text = copy(tx = s :: tx, pos = pos + s.length)
+    def blanks(wd: Int): Text = string(" " * wd)
+    def content: String = tx.reverse.mkString
+  }
+
+  private def breakdist(trees: List[XML.Tree], after: Int): Int =
+    trees match {
+      case Break(_) :: _ => 0
+      case FBreak() :: _ => 0
+      case XML.Elem(_, _, body) :: ts =>
+        (0 /: body)(_ + XML.content_length(_)) + breakdist(ts, after)
+      case XML.Text(s) :: ts => s.length + breakdist(ts, after)
+      case Nil => after
+    }
+
+  private def forcenext(trees: List[XML.Tree]): List[XML.Tree] =
+    trees match {
+      case Nil => Nil
+      case FBreak() :: _ => trees
+      case Break(_) :: ts => FBreak() :: ts
+      case t :: ts => t :: forcenext(ts)
+    }
+
+  def string_of(input: List[XML.Tree], margin: Int = 76): String =
+  {
+    val breakgain = margin / 20
+    val emergencypos = margin / 2
+
+    def format(trees: List[XML.Tree], blockin: Int, after: Int, text: Text): Text =
+      trees match {
+        case Nil => text
+
+        case Block(indent, body) :: ts =>
+          val pos1 = text.pos + indent
+          val pos2 = pos1 % emergencypos
+          val blockin1 =
+            if (pos1 < emergencypos) pos1
+            else pos2
+          val btext = format(body, blockin1, breakdist(ts, after), text)
+          val ts1 = if (text.nl < btext.nl) forcenext(ts) else ts
+          format(ts1, blockin, after, btext)
+
+        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))
+        case FBreak() :: ts => format(ts, blockin, after, text.newline.blanks(blockin))
+
+        case XML.Elem(_, _, body) :: ts => format(body ::: ts, blockin, after, text)
+        case XML.Text(s) :: ts => format(ts, blockin, after, text.string(s))
+      }
+    format(input, 0, 0, Text()).content
+  }
 }