# HG changeset patch
# User wenzelm
# Date 1450563407 -3600
# Node ID 2cb4a29709416ff18a29c8c3376cf7e4954da6c1
# Parent  26f976d5dc4a5e37951a3394fa01267130337dbc
more explicit Pretty.Tree, like in ML;
tuned;

diff -r 26f976d5dc4a -r 2cb4a2970941 src/Pure/General/pretty.scala
--- a/src/Pure/General/pretty.scala	Sat Dec 19 22:25:01 2015 +0100
+++ b/src/Pure/General/pretty.scala	Sat Dec 19 23:16:47 2015 +0100
@@ -9,13 +9,23 @@
 
 object Pretty
 {
-  /* spaces */
+  /* XML constructors */
+
+  def spaces(n: Int): XML.Body = if (n == 0) Nil else List(XML.Text(Symbol.spaces(n)))
+  val space: XML.Body = spaces(1)
 
-  def spaces(n: Int): XML.Body =
-    if (n == 0) Nil
-    else List(XML.Text(Symbol.spaces(n)))
+  def block(consistent: Boolean, indent: Int, body: XML.Body): XML.Tree =
+    XML.Elem(Markup.Block(consistent, indent), body)
+  def block(indent: Int, body: XML.Body): XML.Tree = block(false, indent, body)
+  def block(body: XML.Body): XML.Tree = block(2, body)
 
-  val space: XML.Body = spaces(1)
+  def brk(width: Int, indent: Int = 0): XML.Tree =
+    XML.Elem(Markup.Break(width, indent), spaces(width))
+
+  val fbrk: XML.Tree = XML.Text("\n")
+
+  val Separator: XML.Body = List(XML.elem(Markup.SEPARATOR, space), fbrk)
+  def separate(ts: List[XML.Tree]): XML.Body = Library.separate(Separator, ts.map(List(_))).flatten
 
 
   /* text metric -- standardized to width of space */
@@ -24,8 +34,6 @@
   {
     val unit: Double
     def apply(s: String): Double
-    def content_length(body: XML.Body): Double =
-      XML.traverse_text(body)(0.0)(_ + apply(_))
   }
 
   object Metric_Default extends Metric
@@ -37,51 +45,41 @@
 
   /* markup trees with physical blocks and breaks */
 
-  def block(body: XML.Body): XML.Tree = Block(false, 2, body)
-
-  object Block
-  {
-    def apply(consistent: Boolean, indent: Int, body: XML.Body): XML.Tree =
-      XML.Elem(Markup.Block(consistent, indent), body)
+  sealed abstract class Tree { def length: Double }
+  case class Block(
+    markup: Option[(Markup, Option[XML.Body])],
+    consistent: Boolean, indent: Int, body: List[Tree], length: Double) extends Tree
+  case class Str(string: String, length: Double) extends Tree
+  case class Break(force: Boolean, width: Int, indent: Int) extends Tree
+  { def length: Double = width.toDouble }
 
-    def unapply(tree: XML.Tree): Option[(Boolean, Int, XML.Body)] =
-      tree match {
-        case XML.Elem(Markup.Block(consistent, indent), body) => Some((consistent, indent, body))
-        case _ => None
-      }
-  }
+  val FBreak = Break(true, 1, 0)
 
-  object Break
-  {
-    def apply(w: Int, i: Int = 0): XML.Tree =
-      XML.Elem(Markup.Break(w, i), spaces(w))
+  def make_block(
+      markup: Option[(Markup, Option[XML.Body])],
+      consistent: Boolean,
+      indent: Int,
+      body: List[Tree]): Tree =
+    Block(markup, consistent, indent, body, (0.0 /: body) { case (n, t) => n + t.length })
 
-    def unapply(tree: XML.Tree): Option[(Int, Int)] =
-      tree match {
-        case XML.Elem(Markup.Break(w, i), _) => Some((w, i))
-        case _ => None
-      }
-  }
-
-  val FBreak = XML.Text("\n")
-
-  def item(body: XML.Body): XML.Tree =
-    Block(false, 2, XML.elem(Markup.BULLET, space) :: space ::: body)
-
-  val Separator = List(XML.elem(Markup.SEPARATOR, space), FBreak)
-  def separate(ts: List[XML.Tree]): XML.Body = Library.separate(Separator, ts.map(List(_))).flatten
-
-
-  /* standard form */
-
-  def standard_form(body: XML.Body): XML.Body =
-    body flatMap {
+  def make_tree(metric: Metric, xml: XML.Body): List[Tree] =
+    xml flatMap {
       case XML.Wrapped_Elem(markup, body1, body2) =>
-        List(XML.Wrapped_Elem(markup, body1, standard_form(body2)))
+        List(make_block(Some(markup, Some(body1)), false, 0, make_tree(metric, body2)))
       case XML.Elem(markup, body) =>
-        if (markup.name == Markup.ITEM) List(item(standard_form(body)))
-        else List(XML.Elem(markup, standard_form(body)))
-      case XML.Text(text) => Library.separate(FBreak, split_lines(text).map(XML.Text))
+        markup match {
+          case Markup.Block(consistent, indent) =>
+            List(make_block(None, consistent, indent, make_tree(metric, body)))
+          case Markup.Break(width, indent) =>
+            List(Break(false, width, indent))
+          case Markup(Markup.ITEM, _) =>
+            List(make_block(None, false, 2,
+              make_tree(metric, XML.elem(Markup.BULLET, space) :: space ::: body)))
+          case _ =>
+            List(make_block(Some((markup, None)), false, 0, make_tree(metric, body)))
+        }
+      case XML.Text(text) =>
+        Library.separate(FBreak, split_lines(text).map(s => Str(s, metric(s))))
     }
 
 
@@ -94,76 +92,68 @@
   {
     sealed case class Text(tx: XML.Body = Nil, pos: Double = 0.0, nl: Int = 0)
     {
-      def newline: Text = copy(tx = FBreak :: tx, pos = 0.0, nl = nl + 1)
-      def string(s: String): Text =
-        if (s == "") this
-        else copy(tx = XML.Text(s) :: tx, pos = pos + metric(s))
-      def blanks(wd: Int): Text = string(Symbol.spaces(wd))
+      def newline: Text = copy(tx = fbrk :: tx, pos = 0.0, nl = nl + 1)
+      def string(s: String, len: Double): Text =
+        copy(tx = if (s == "") tx else XML.Text(s) :: tx, pos = pos + len)
+      def blanks(wd: Int): Text = string(Symbol.spaces(wd), wd.toDouble)
       def content: XML.Body = tx.reverse
     }
 
     val breakgain = margin / 20
     val emergencypos = (margin / 2).round.toInt
 
-    def break_dist(trees: XML.Body, after: Double): Double =
+    def break_dist(trees: List[Tree], after: Double): Double =
       trees match {
-        case Break(_, _) :: _ => 0.0
-        case FBreak :: _ => 0.0
-        case t :: ts => metric.content_length(List(t)) + break_dist(ts, after)
+        case (_: Break) :: _ => 0.0
+        case t :: ts => t.length + break_dist(ts, after)
         case Nil => after
       }
 
-    def force_all(trees: XML.Body): XML.Body =
-      trees flatMap {
-        case Break(_, ind) => FBreak :: spaces(ind)
-        case tree => List(tree)
-      }
+    def force_break(tree: Tree): Tree =
+      tree match { case Break(false, wd, ind) => Break(true, wd, ind) case _ => tree }
+    def force_all(trees: List[Tree]): List[Tree] = trees.map(force_break(_))
 
-    def force_next(trees: XML.Body): XML.Body =
+    def force_next(trees: List[Tree]): List[Tree] =
       trees match {
         case Nil => Nil
-        case FBreak :: _ => trees
-        case Break(_, ind) :: ts => FBreak :: spaces(ind) ::: ts
+        case (t: Break) :: ts => force_break(t) :: ts
         case t :: ts => t :: force_next(ts)
       }
 
-    def format(trees: XML.Body, blockin: Int, after: Double, text: Text): Text =
+    def format(trees: List[Tree], blockin: Int, after: Double, text: Text): Text =
       trees match {
         case Nil => text
 
-        case Block(consistent, indent, body) :: ts =>
+        case Block(markup, consistent, indent, body, blen) :: ts =>
           val pos1 = (text.pos + indent).ceil.toInt
           val pos2 = pos1 % emergencypos
           val blockin1 = if (pos1 < emergencypos) pos1 else pos2
-          val blen = metric.content_length(body)
           val d = break_dist(ts, after)
           val body1 = if (consistent && text.pos + blen > margin - d) force_all(body) else body
-          val btext = format(body1, blockin1, d, text)
+          val btext =
+            markup match {
+              case None => format(body1, blockin1, d, text)
+              case Some((m, markup_body)) =>
+                val btext0 = format(body1, blockin1, d, text.copy(tx = Nil))
+                val elem =
+                  markup_body match {
+                    case None => XML.Elem(m, btext0.content)
+                    case Some(b) => XML.Wrapped_Elem(m, b, btext0.content)
+                  }
+                btext0.copy(tx = elem :: text.tx)
+            }
           val ts1 = if (text.nl < btext.nl) force_next(ts) else ts
           format(ts1, blockin, after, btext)
 
-        case Break(wd, ind) :: ts =>
-          if (text.pos + wd <= ((margin - break_dist(ts, after)) max (blockin + breakgain)))
+        case Break(force, wd, ind) :: ts =>
+          if (!force &&
+              text.pos + wd <= ((margin - break_dist(ts, after)) max (blockin + breakgain)))
             format(ts, blockin, after, text.blanks(wd))
           else format(ts, blockin, after, text.newline.blanks(blockin + ind))
-        case FBreak :: ts => format(ts, blockin, after, text.newline.blanks(blockin))
 
-        case XML.Wrapped_Elem(markup, body1, body2) :: ts =>
-          val btext = format(body2, blockin, break_dist(ts, after), text.copy(tx = Nil))
-          val ts1 = if (text.nl < btext.nl) force_next(ts) else ts
-          val btext1 = btext.copy(tx = XML.Wrapped_Elem(markup, body1, btext.content) :: text.tx)
-          format(ts1, blockin, after, btext1)
-
-        case XML.Elem(markup, body) :: ts =>
-          val btext = format(body, blockin, break_dist(ts, after), text.copy(tx = Nil))
-          val ts1 = if (text.nl < btext.nl) force_next(ts) else ts
-          val btext1 = btext.copy(tx = XML.Elem(markup, btext.content) :: text.tx)
-          format(ts1, blockin, after, btext1)
-
-        case XML.Text(s) :: ts => format(ts, blockin, after, text.string(s))
+        case Str(s, len) :: ts => format(ts, blockin, after, text.string(s, len))
       }
-
-    format(standard_form(input), 0, 0.0, Text()).content
+    format(make_tree(metric, input), 0, 0.0, Text()).content
   }
 
   def string_of(input: XML.Body, margin: Double = margin_default,
@@ -177,15 +167,17 @@
   {
     def fmt(tree: XML.Tree): XML.Body =
       tree match {
-        case Block(_, _, body) => body.flatMap(fmt)
-        case Break(wd, _) => spaces(wd)
-        case FBreak => space
         case XML.Wrapped_Elem(markup, body1, body2) =>
           List(XML.Wrapped_Elem(markup, body1, body2.flatMap(fmt)))
-        case XML.Elem(markup, body) => List(XML.Elem(markup, body.flatMap(fmt)))
-        case XML.Text(_) => List(tree)
+        case XML.Elem(markup, body) =>
+          markup match {
+            case Markup.Block(_, _) => body.flatMap(fmt)
+            case Markup.Break(wd, _) => spaces(wd)
+            case _ => List(XML.Elem(markup, body.flatMap(fmt)))
+          }
+        case XML.Text(s) => List(XML.Text(s.replace('\n', ' ')))
       }
-    standard_form(input).flatMap(fmt)
+    input.flatMap(fmt)
   }
 
   def str_of(input: XML.Body): String = XML.content(unformatted(input))
diff -r 26f976d5dc4a -r 2cb4a2970941 src/Tools/jEdit/src/isabelle_sidekick.scala
--- a/src/Tools/jEdit/src/isabelle_sidekick.scala	Sat Dec 19 22:25:01 2015 +0100
+++ b/src/Tools/jEdit/src/isabelle_sidekick.scala	Sat Dec 19 23:16:47 2015 +0100
@@ -179,7 +179,7 @@
                 val range = info.range + command_start
                 val content = command.source(info.range).replace('\n', ' ')
                 val info_text =
-                  Pretty.formatted(Library.separate(Pretty.FBreak, info.info), margin = 40.0)
+                  Pretty.formatted(Library.separate(Pretty.fbrk, info.info), margin = 40.0)
                     .mkString
 
                 new DefaultMutableTreeNode(
diff -r 26f976d5dc4a -r 2cb4a2970941 src/Tools/jEdit/src/rendering.scala
--- a/src/Tools/jEdit/src/rendering.scala	Sat Dec 19 22:25:01 2015 +0100
+++ b/src/Tools/jEdit/src/rendering.scala	Sat Dec 19 23:16:47 2015 +0100
@@ -506,7 +506,7 @@
   /* tooltips */
 
   private def pretty_typing(kind: String, body: XML.Body): XML.Tree =
-    Pretty.block(XML.Text(kind) :: Pretty.Break(1) :: body)
+    Pretty.block(XML.Text(kind) :: Pretty.brk(1) :: body)
 
   private def timing_threshold: Double = options.real("jedit_timing_threshold")
 
@@ -585,7 +585,7 @@
       case tips =>
         val r = Text.Range(results.head.range.start, results.last.range.stop)
         val all_tips = (tips.filter(_._1) ++ tips.filter(!_._1).lastOption.toList).map(_._2)
-        Some(Text.Info(r, Library.separate(Pretty.FBreak, all_tips)))
+        Some(Text.Info(r, Library.separate(Pretty.fbrk, all_tips)))
     }
   }