src/Pure/General/pretty.scala
author wenzelm
Sat, 02 Apr 2016 21:54:51 +0200
changeset 62820 5c678ee5d34a
parent 62785 70b9c7d4ed7f
child 65130 695930882487
permissions -rw-r--r--
proper type; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
36683
41a1210519fd basic support for symbolic pretty printing;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/General/pretty.scala
41a1210519fd basic support for symbolic pretty printing;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
41a1210519fd basic support for symbolic pretty printing;
wenzelm
parents:
diff changeset
     3
36687
58020b59baf7 basic formatting of pretty trees;
wenzelm
parents: 36683
diff changeset
     4
Generic pretty printing module.
36683
41a1210519fd basic support for symbolic pretty printing;
wenzelm
parents:
diff changeset
     5
*/
41a1210519fd basic support for symbolic pretty printing;
wenzelm
parents:
diff changeset
     6
41a1210519fd basic support for symbolic pretty printing;
wenzelm
parents:
diff changeset
     7
package isabelle
41a1210519fd basic support for symbolic pretty printing;
wenzelm
parents:
diff changeset
     8
41a1210519fd basic support for symbolic pretty printing;
wenzelm
parents:
diff changeset
     9
41a1210519fd basic support for symbolic pretty printing;
wenzelm
parents:
diff changeset
    10
object Pretty
41a1210519fd basic support for symbolic pretty printing;
wenzelm
parents:
diff changeset
    11
{
61871
2cb4a2970941 more explicit Pretty.Tree, like in ML;
wenzelm
parents: 61868
diff changeset
    12
  /* XML constructors */
2cb4a2970941 more explicit Pretty.Tree, like in ML;
wenzelm
parents: 61868
diff changeset
    13
61874
wenzelm
parents: 61871
diff changeset
    14
  val space: XML.Body = List(XML.Text(Symbol.space))
wenzelm
parents: 61871
diff changeset
    15
  def spaces(n: Int): XML.Body =
wenzelm
parents: 61871
diff changeset
    16
    if (n == 0) Nil
wenzelm
parents: 61871
diff changeset
    17
    else if (n == 1) space
wenzelm
parents: 61871
diff changeset
    18
    else List(XML.Text(Symbol.spaces(n)))
48704
85a3de10567d tuned signature -- make Pretty less dependent on Symbol;
wenzelm
parents: 45666
diff changeset
    19
61871
2cb4a2970941 more explicit Pretty.Tree, like in ML;
wenzelm
parents: 61868
diff changeset
    20
  def block(consistent: Boolean, indent: Int, body: XML.Body): XML.Tree =
2cb4a2970941 more explicit Pretty.Tree, like in ML;
wenzelm
parents: 61868
diff changeset
    21
    XML.Elem(Markup.Block(consistent, indent), body)
2cb4a2970941 more explicit Pretty.Tree, like in ML;
wenzelm
parents: 61868
diff changeset
    22
  def block(indent: Int, body: XML.Body): XML.Tree = block(false, indent, body)
2cb4a2970941 more explicit Pretty.Tree, like in ML;
wenzelm
parents: 61868
diff changeset
    23
  def block(body: XML.Body): XML.Tree = block(2, body)
48704
85a3de10567d tuned signature -- make Pretty less dependent on Symbol;
wenzelm
parents: 45666
diff changeset
    24
61871
2cb4a2970941 more explicit Pretty.Tree, like in ML;
wenzelm
parents: 61868
diff changeset
    25
  def brk(width: Int, indent: Int = 0): XML.Tree =
2cb4a2970941 more explicit Pretty.Tree, like in ML;
wenzelm
parents: 61868
diff changeset
    26
    XML.Elem(Markup.Break(width, indent), spaces(width))
2cb4a2970941 more explicit Pretty.Tree, like in ML;
wenzelm
parents: 61868
diff changeset
    27
2cb4a2970941 more explicit Pretty.Tree, like in ML;
wenzelm
parents: 61868
diff changeset
    28
  val fbrk: XML.Tree = XML.Text("\n")
2cb4a2970941 more explicit Pretty.Tree, like in ML;
wenzelm
parents: 61868
diff changeset
    29
2cb4a2970941 more explicit Pretty.Tree, like in ML;
wenzelm
parents: 61868
diff changeset
    30
  val Separator: XML.Body = List(XML.elem(Markup.SEPARATOR, space), fbrk)
2cb4a2970941 more explicit Pretty.Tree, like in ML;
wenzelm
parents: 61868
diff changeset
    31
  def separate(ts: List[XML.Tree]): XML.Body = Library.separate(Separator, ts.map(List(_))).flatten
61864
3a5992c3410c support for blocks with consistent breaks;
wenzelm
parents: 61862
diff changeset
    32
48704
85a3de10567d tuned signature -- make Pretty less dependent on Symbol;
wenzelm
parents: 45666
diff changeset
    33
51492
eaa1c4cc1106 more explicit Pretty.Metric, with clear distinction of unit (space width) vs. average char width (for visual adjustments) -- NB: Pretty formatting works via full space characters (despite a981a5c8a505 and 70f7483df9cb);
wenzelm
parents: 51470
diff changeset
    34
  /* text metric -- standardized to width of space */
eaa1c4cc1106 more explicit Pretty.Metric, with clear distinction of unit (space width) vs. average char width (for visual adjustments) -- NB: Pretty formatting works via full space characters (despite a981a5c8a505 and 70f7483df9cb);
wenzelm
parents: 51470
diff changeset
    35
eaa1c4cc1106 more explicit Pretty.Metric, with clear distinction of unit (space width) vs. average char width (for visual adjustments) -- NB: Pretty formatting works via full space characters (despite a981a5c8a505 and 70f7483df9cb);
wenzelm
parents: 51470
diff changeset
    36
  abstract class Metric
eaa1c4cc1106 more explicit Pretty.Metric, with clear distinction of unit (space width) vs. average char width (for visual adjustments) -- NB: Pretty formatting works via full space characters (despite a981a5c8a505 and 70f7483df9cb);
wenzelm
parents: 51470
diff changeset
    37
  {
eaa1c4cc1106 more explicit Pretty.Metric, with clear distinction of unit (space width) vs. average char width (for visual adjustments) -- NB: Pretty formatting works via full space characters (despite a981a5c8a505 and 70f7483df9cb);
wenzelm
parents: 51470
diff changeset
    38
    val unit: Double
eaa1c4cc1106 more explicit Pretty.Metric, with clear distinction of unit (space width) vs. average char width (for visual adjustments) -- NB: Pretty formatting works via full space characters (despite a981a5c8a505 and 70f7483df9cb);
wenzelm
parents: 51470
diff changeset
    39
    def apply(s: String): Double
eaa1c4cc1106 more explicit Pretty.Metric, with clear distinction of unit (space width) vs. average char width (for visual adjustments) -- NB: Pretty formatting works via full space characters (despite a981a5c8a505 and 70f7483df9cb);
wenzelm
parents: 51470
diff changeset
    40
  }
eaa1c4cc1106 more explicit Pretty.Metric, with clear distinction of unit (space width) vs. average char width (for visual adjustments) -- NB: Pretty formatting works via full space characters (despite a981a5c8a505 and 70f7483df9cb);
wenzelm
parents: 51470
diff changeset
    41
eaa1c4cc1106 more explicit Pretty.Metric, with clear distinction of unit (space width) vs. average char width (for visual adjustments) -- NB: Pretty formatting works via full space characters (despite a981a5c8a505 and 70f7483df9cb);
wenzelm
parents: 51470
diff changeset
    42
  object Metric_Default extends Metric
eaa1c4cc1106 more explicit Pretty.Metric, with clear distinction of unit (space width) vs. average char width (for visual adjustments) -- NB: Pretty formatting works via full space characters (despite a981a5c8a505 and 70f7483df9cb);
wenzelm
parents: 51470
diff changeset
    43
  {
eaa1c4cc1106 more explicit Pretty.Metric, with clear distinction of unit (space width) vs. average char width (for visual adjustments) -- NB: Pretty formatting works via full space characters (despite a981a5c8a505 and 70f7483df9cb);
wenzelm
parents: 51470
diff changeset
    44
    val unit = 1.0
eaa1c4cc1106 more explicit Pretty.Metric, with clear distinction of unit (space width) vs. average char width (for visual adjustments) -- NB: Pretty formatting works via full space characters (despite a981a5c8a505 and 70f7483df9cb);
wenzelm
parents: 51470
diff changeset
    45
    def apply(s: String): Double = s.length.toDouble
eaa1c4cc1106 more explicit Pretty.Metric, with clear distinction of unit (space width) vs. average char width (for visual adjustments) -- NB: Pretty formatting works via full space characters (despite a981a5c8a505 and 70f7483df9cb);
wenzelm
parents: 51470
diff changeset
    46
  }
eaa1c4cc1106 more explicit Pretty.Metric, with clear distinction of unit (space width) vs. average char width (for visual adjustments) -- NB: Pretty formatting works via full space characters (despite a981a5c8a505 and 70f7483df9cb);
wenzelm
parents: 51470
diff changeset
    47
eaa1c4cc1106 more explicit Pretty.Metric, with clear distinction of unit (space width) vs. average char width (for visual adjustments) -- NB: Pretty formatting works via full space characters (despite a981a5c8a505 and 70f7483df9cb);
wenzelm
parents: 51470
diff changeset
    48
36687
58020b59baf7 basic formatting of pretty trees;
wenzelm
parents: 36683
diff changeset
    49
  /* markup trees with physical blocks and breaks */
58020b59baf7 basic formatting of pretty trees;
wenzelm
parents: 36683
diff changeset
    50
62820
5c678ee5d34a proper type;
wenzelm
parents: 62785
diff changeset
    51
  private def force_nat(i: Int): Int = i max 0
5c678ee5d34a proper type;
wenzelm
parents: 62785
diff changeset
    52
61874
wenzelm
parents: 61871
diff changeset
    53
  private sealed abstract class Tree { def length: Double }
wenzelm
parents: 61871
diff changeset
    54
  private case class Block(
61871
2cb4a2970941 more explicit Pretty.Tree, like in ML;
wenzelm
parents: 61868
diff changeset
    55
    markup: Option[(Markup, Option[XML.Body])],
2cb4a2970941 more explicit Pretty.Tree, like in ML;
wenzelm
parents: 61868
diff changeset
    56
    consistent: Boolean, indent: Int, body: List[Tree], length: Double) extends Tree
61874
wenzelm
parents: 61871
diff changeset
    57
  private case class Break(force: Boolean, width: Int, indent: Int) extends Tree
61871
2cb4a2970941 more explicit Pretty.Tree, like in ML;
wenzelm
parents: 61868
diff changeset
    58
  { def length: Double = width.toDouble }
61874
wenzelm
parents: 61871
diff changeset
    59
  private case class Str(string: String, length: Double) extends Tree
36683
41a1210519fd basic support for symbolic pretty printing;
wenzelm
parents:
diff changeset
    60
61874
wenzelm
parents: 61871
diff changeset
    61
  private val FBreak = Break(true, 1, 0)
36683
41a1210519fd basic support for symbolic pretty printing;
wenzelm
parents:
diff changeset
    62
61874
wenzelm
parents: 61871
diff changeset
    63
  private def make_block(
61871
2cb4a2970941 more explicit Pretty.Tree, like in ML;
wenzelm
parents: 61868
diff changeset
    64
      markup: Option[(Markup, Option[XML.Body])],
2cb4a2970941 more explicit Pretty.Tree, like in ML;
wenzelm
parents: 61868
diff changeset
    65
      consistent: Boolean,
2cb4a2970941 more explicit Pretty.Tree, like in ML;
wenzelm
parents: 61868
diff changeset
    66
      indent: Int,
2cb4a2970941 more explicit Pretty.Tree, like in ML;
wenzelm
parents: 61868
diff changeset
    67
      body: List[Tree]): Tree =
61883
c0f34fe6aa61 clarified length of block with pre-existant forced breaks;
wenzelm
parents: 61875
diff changeset
    68
  {
62785
70b9c7d4ed7f more robust pretty printing: permissive treatment of bad values;
wenzelm
parents: 61883
diff changeset
    69
    val indent1 = force_nat(indent)
70b9c7d4ed7f more robust pretty printing: permissive treatment of bad values;
wenzelm
parents: 61883
diff changeset
    70
61883
c0f34fe6aa61 clarified length of block with pre-existant forced breaks;
wenzelm
parents: 61875
diff changeset
    71
    def body_length(prts: List[Tree], len: Double): Double =
c0f34fe6aa61 clarified length of block with pre-existant forced breaks;
wenzelm
parents: 61875
diff changeset
    72
    {
c0f34fe6aa61 clarified length of block with pre-existant forced breaks;
wenzelm
parents: 61875
diff changeset
    73
      val (line, rest) =
c0f34fe6aa61 clarified length of block with pre-existant forced breaks;
wenzelm
parents: 61875
diff changeset
    74
        Library.take_prefix[Tree]({ case Break(true, _, _) => false case _ => true }, prts)
c0f34fe6aa61 clarified length of block with pre-existant forced breaks;
wenzelm
parents: 61875
diff changeset
    75
      val len1 = ((0.0 /: line) { case (l, t) => l + t.length }) max len
c0f34fe6aa61 clarified length of block with pre-existant forced breaks;
wenzelm
parents: 61875
diff changeset
    76
      rest match {
c0f34fe6aa61 clarified length of block with pre-existant forced breaks;
wenzelm
parents: 61875
diff changeset
    77
        case Break(true, _, ind) :: rest1 =>
62785
70b9c7d4ed7f more robust pretty printing: permissive treatment of bad values;
wenzelm
parents: 61883
diff changeset
    78
          body_length(Break(false, indent1 + ind, 0) :: rest1, len1)
61883
c0f34fe6aa61 clarified length of block with pre-existant forced breaks;
wenzelm
parents: 61875
diff changeset
    79
        case Nil => len1
c0f34fe6aa61 clarified length of block with pre-existant forced breaks;
wenzelm
parents: 61875
diff changeset
    80
      }
c0f34fe6aa61 clarified length of block with pre-existant forced breaks;
wenzelm
parents: 61875
diff changeset
    81
    }
62785
70b9c7d4ed7f more robust pretty printing: permissive treatment of bad values;
wenzelm
parents: 61883
diff changeset
    82
    Block(markup, consistent, indent1, body, body_length(body, 0.0))
61883
c0f34fe6aa61 clarified length of block with pre-existant forced breaks;
wenzelm
parents: 61875
diff changeset
    83
  }
36683
41a1210519fd basic support for symbolic pretty printing;
wenzelm
parents:
diff changeset
    84
61874
wenzelm
parents: 61871
diff changeset
    85
wenzelm
parents: 61871
diff changeset
    86
  /* formatted output */
wenzelm
parents: 61871
diff changeset
    87
wenzelm
parents: 61871
diff changeset
    88
  private sealed case class Text(tx: XML.Body = Nil, pos: Double = 0.0, nl: Int = 0)
wenzelm
parents: 61871
diff changeset
    89
  {
wenzelm
parents: 61871
diff changeset
    90
    def newline: Text = copy(tx = fbrk :: tx, pos = 0.0, nl = nl + 1)
wenzelm
parents: 61871
diff changeset
    91
    def string(s: String, len: Double): Text =
wenzelm
parents: 61871
diff changeset
    92
      copy(tx = if (s == "") tx else XML.Text(s) :: tx, pos = pos + len)
wenzelm
parents: 61871
diff changeset
    93
    def blanks(wd: Int): Text = string(Symbol.spaces(wd), wd.toDouble)
wenzelm
parents: 61871
diff changeset
    94
    def content: XML.Body = tx.reverse
wenzelm
parents: 61871
diff changeset
    95
  }
wenzelm
parents: 61871
diff changeset
    96
wenzelm
parents: 61871
diff changeset
    97
  private def break_dist(trees: List[Tree], after: Double): Double =
wenzelm
parents: 61871
diff changeset
    98
    trees match {
wenzelm
parents: 61871
diff changeset
    99
      case (_: Break) :: _ => 0.0
wenzelm
parents: 61871
diff changeset
   100
      case t :: ts => t.length + break_dist(ts, after)
wenzelm
parents: 61871
diff changeset
   101
      case Nil => after
36689
379f5b1e7f91 replaced slightly odd fbreak markup by plain "\n", which also coincides with regular linebreaks produced outside the ML pretty engine;
wenzelm
parents: 36687
diff changeset
   102
    }
379f5b1e7f91 replaced slightly odd fbreak markup by plain "\n", which also coincides with regular linebreaks produced outside the ML pretty engine;
wenzelm
parents: 36687
diff changeset
   103
61874
wenzelm
parents: 61871
diff changeset
   104
  private def force_break(tree: Tree): Tree =
wenzelm
parents: 61871
diff changeset
   105
    tree match { case Break(false, wd, ind) => Break(true, wd, ind) case _ => tree }
wenzelm
parents: 61871
diff changeset
   106
  private def force_all(trees: List[Tree]): List[Tree] = trees.map(force_break(_))
51570
3633828d80fc basic support for Pretty.item, which is considered as logical markup and interpreted in Isabelle/Scala, but ignored elsewhere (TTY, latex etc.);
wenzelm
parents: 51569
diff changeset
   107
61874
wenzelm
parents: 61871
diff changeset
   108
  private def force_next(trees: List[Tree]): List[Tree] =
wenzelm
parents: 61871
diff changeset
   109
    trees match {
wenzelm
parents: 61871
diff changeset
   110
      case Nil => Nil
wenzelm
parents: 61871
diff changeset
   111
      case (t: Break) :: ts => force_break(t) :: ts
wenzelm
parents: 61871
diff changeset
   112
      case t :: ts => t :: force_next(ts)
wenzelm
parents: 61871
diff changeset
   113
    }
51570
3633828d80fc basic support for Pretty.item, which is considered as logical markup and interpreted in Isabelle/Scala, but ignored elsewhere (TTY, latex etc.);
wenzelm
parents: 51569
diff changeset
   114
51493
59d8a1031c00 allow fractional pretty margin -- avoid premature rounding;
wenzelm
parents: 51492
diff changeset
   115
  private val margin_default = 76.0
36820
0cdfce0bf956 clarified Pretty.font_metrics;
wenzelm
parents: 36818
diff changeset
   116
51493
59d8a1031c00 allow fractional pretty margin -- avoid premature rounding;
wenzelm
parents: 51492
diff changeset
   117
  def formatted(input: XML.Body, margin: Double = margin_default,
51492
eaa1c4cc1106 more explicit Pretty.Metric, with clear distinction of unit (space width) vs. average char width (for visual adjustments) -- NB: Pretty formatting works via full space characters (despite a981a5c8a505 and 70f7483df9cb);
wenzelm
parents: 51470
diff changeset
   118
    metric: Metric = Metric_Default): XML.Body =
36687
58020b59baf7 basic formatting of pretty trees;
wenzelm
parents: 36683
diff changeset
   119
  {
58020b59baf7 basic formatting of pretty trees;
wenzelm
parents: 36683
diff changeset
   120
    val breakgain = margin / 20
51569
4e084727faae maintain integer indentation during formatting -- it needs to be implemented by repeated spaces eventually;
wenzelm
parents: 51568
diff changeset
   121
    val emergencypos = (margin / 2).round.toInt
36687
58020b59baf7 basic formatting of pretty trees;
wenzelm
parents: 36683
diff changeset
   122
61874
wenzelm
parents: 61871
diff changeset
   123
    def make_tree(inp: XML.Body): List[Tree] =
wenzelm
parents: 61871
diff changeset
   124
      inp flatMap {
wenzelm
parents: 61871
diff changeset
   125
        case XML.Wrapped_Elem(markup, body1, body2) =>
wenzelm
parents: 61871
diff changeset
   126
          List(make_block(Some(markup, Some(body1)), false, 0, make_tree(body2)))
wenzelm
parents: 61871
diff changeset
   127
        case XML.Elem(markup, body) =>
wenzelm
parents: 61871
diff changeset
   128
          markup match {
wenzelm
parents: 61871
diff changeset
   129
            case Markup.Block(consistent, indent) =>
wenzelm
parents: 61871
diff changeset
   130
              List(make_block(None, consistent, indent, make_tree(body)))
wenzelm
parents: 61871
diff changeset
   131
            case Markup.Break(width, indent) =>
62785
70b9c7d4ed7f more robust pretty printing: permissive treatment of bad values;
wenzelm
parents: 61883
diff changeset
   132
              List(Break(false, force_nat(width), force_nat(indent)))
61874
wenzelm
parents: 61871
diff changeset
   133
            case Markup(Markup.ITEM, _) =>
wenzelm
parents: 61871
diff changeset
   134
              List(make_block(None, false, 2,
wenzelm
parents: 61871
diff changeset
   135
                make_tree(XML.elem(Markup.BULLET, space) :: space ::: body)))
wenzelm
parents: 61871
diff changeset
   136
            case _ =>
wenzelm
parents: 61871
diff changeset
   137
              List(make_block(Some((markup, None)), false, 0, make_tree(body)))
wenzelm
parents: 61871
diff changeset
   138
          }
wenzelm
parents: 61871
diff changeset
   139
        case XML.Text(text) =>
wenzelm
parents: 61871
diff changeset
   140
          Library.separate(FBreak, split_lines(text).map(s => Str(s, metric(s))))
36817
ed97e877ff2d more precise pretty printing based on actual font metrics;
wenzelm
parents: 36763
diff changeset
   141
      }
ed97e877ff2d more precise pretty printing based on actual font metrics;
wenzelm
parents: 36763
diff changeset
   142
61871
2cb4a2970941 more explicit Pretty.Tree, like in ML;
wenzelm
parents: 61868
diff changeset
   143
    def format(trees: List[Tree], blockin: Int, after: Double, text: Text): Text =
36687
58020b59baf7 basic formatting of pretty trees;
wenzelm
parents: 36683
diff changeset
   144
      trees match {
58020b59baf7 basic formatting of pretty trees;
wenzelm
parents: 36683
diff changeset
   145
        case Nil => text
58020b59baf7 basic formatting of pretty trees;
wenzelm
parents: 36683
diff changeset
   146
61871
2cb4a2970941 more explicit Pretty.Tree, like in ML;
wenzelm
parents: 61868
diff changeset
   147
        case Block(markup, consistent, indent, body, blen) :: ts =>
51569
4e084727faae maintain integer indentation during formatting -- it needs to be implemented by repeated spaces eventually;
wenzelm
parents: 51568
diff changeset
   148
          val pos1 = (text.pos + indent).ceil.toInt
36687
58020b59baf7 basic formatting of pretty trees;
wenzelm
parents: 36683
diff changeset
   149
          val pos2 = pos1 % emergencypos
61868
wenzelm
parents: 61865
diff changeset
   150
          val blockin1 = if (pos1 < emergencypos) pos1 else pos2
61864
3a5992c3410c support for blocks with consistent breaks;
wenzelm
parents: 61862
diff changeset
   151
          val d = break_dist(ts, after)
3a5992c3410c support for blocks with consistent breaks;
wenzelm
parents: 61862
diff changeset
   152
          val body1 = if (consistent && text.pos + blen > margin - d) force_all(body) else body
61871
2cb4a2970941 more explicit Pretty.Tree, like in ML;
wenzelm
parents: 61868
diff changeset
   153
          val btext =
2cb4a2970941 more explicit Pretty.Tree, like in ML;
wenzelm
parents: 61868
diff changeset
   154
            markup match {
2cb4a2970941 more explicit Pretty.Tree, like in ML;
wenzelm
parents: 61868
diff changeset
   155
              case None => format(body1, blockin1, d, text)
2cb4a2970941 more explicit Pretty.Tree, like in ML;
wenzelm
parents: 61868
diff changeset
   156
              case Some((m, markup_body)) =>
2cb4a2970941 more explicit Pretty.Tree, like in ML;
wenzelm
parents: 61868
diff changeset
   157
                val btext0 = format(body1, blockin1, d, text.copy(tx = Nil))
2cb4a2970941 more explicit Pretty.Tree, like in ML;
wenzelm
parents: 61868
diff changeset
   158
                val elem =
2cb4a2970941 more explicit Pretty.Tree, like in ML;
wenzelm
parents: 61868
diff changeset
   159
                  markup_body match {
2cb4a2970941 more explicit Pretty.Tree, like in ML;
wenzelm
parents: 61868
diff changeset
   160
                    case None => XML.Elem(m, btext0.content)
2cb4a2970941 more explicit Pretty.Tree, like in ML;
wenzelm
parents: 61868
diff changeset
   161
                    case Some(b) => XML.Wrapped_Elem(m, b, btext0.content)
2cb4a2970941 more explicit Pretty.Tree, like in ML;
wenzelm
parents: 61868
diff changeset
   162
                  }
2cb4a2970941 more explicit Pretty.Tree, like in ML;
wenzelm
parents: 61868
diff changeset
   163
                btext0.copy(tx = elem :: text.tx)
2cb4a2970941 more explicit Pretty.Tree, like in ML;
wenzelm
parents: 61868
diff changeset
   164
            }
61864
3a5992c3410c support for blocks with consistent breaks;
wenzelm
parents: 61862
diff changeset
   165
          val ts1 = if (text.nl < btext.nl) force_next(ts) else ts
36687
58020b59baf7 basic formatting of pretty trees;
wenzelm
parents: 36683
diff changeset
   166
          format(ts1, blockin, after, btext)
58020b59baf7 basic formatting of pretty trees;
wenzelm
parents: 36683
diff changeset
   167
61871
2cb4a2970941 more explicit Pretty.Tree, like in ML;
wenzelm
parents: 61868
diff changeset
   168
        case Break(force, wd, ind) :: ts =>
2cb4a2970941 more explicit Pretty.Tree, like in ML;
wenzelm
parents: 61868
diff changeset
   169
          if (!force &&
2cb4a2970941 more explicit Pretty.Tree, like in ML;
wenzelm
parents: 61868
diff changeset
   170
              text.pos + wd <= ((margin - break_dist(ts, after)) max (blockin + breakgain)))
36687
58020b59baf7 basic formatting of pretty trees;
wenzelm
parents: 36683
diff changeset
   171
            format(ts, blockin, after, text.blanks(wd))
61862
e2a9e46ac0fb support pretty break indent, like underlying ML systems;
wenzelm
parents: 55551
diff changeset
   172
          else format(ts, blockin, after, text.newline.blanks(blockin + ind))
36687
58020b59baf7 basic formatting of pretty trees;
wenzelm
parents: 36683
diff changeset
   173
61871
2cb4a2970941 more explicit Pretty.Tree, like in ML;
wenzelm
parents: 61868
diff changeset
   174
        case Str(s, len) :: ts => format(ts, blockin, after, text.string(s, len))
36687
58020b59baf7 basic formatting of pretty trees;
wenzelm
parents: 36683
diff changeset
   175
      }
61874
wenzelm
parents: 61871
diff changeset
   176
    format(make_tree(input), 0, 0.0, Text()).content
36687
58020b59baf7 basic formatting of pretty trees;
wenzelm
parents: 36683
diff changeset
   177
  }
36734
d9b10c173330 Pretty.formatted operates directly on XML trees, treating XML.Elem like a pro-forma block of indentation 0, like the ML version;
wenzelm
parents: 36689
diff changeset
   178
51493
59d8a1031c00 allow fractional pretty margin -- avoid premature rounding;
wenzelm
parents: 51492
diff changeset
   179
  def string_of(input: XML.Body, margin: Double = margin_default,
51492
eaa1c4cc1106 more explicit Pretty.Metric, with clear distinction of unit (space width) vs. average char width (for visual adjustments) -- NB: Pretty formatting works via full space characters (despite a981a5c8a505 and 70f7483df9cb);
wenzelm
parents: 51470
diff changeset
   180
      metric: Metric = Metric_Default): String =
49416
1053a564dd25 some actual rich text markup via XML.content_markup;
wenzelm
parents: 49414
diff changeset
   181
    XML.content(formatted(input, margin, metric))
36683
41a1210519fd basic support for symbolic pretty printing;
wenzelm
parents:
diff changeset
   182
}