src/Pure/General/pretty.scala
author wenzelm
Fri Sep 28 22:53:18 2012 +0200 (2012-09-28 ago)
changeset 49650 9fad6480300d
parent 49473 ca7e2c21b104
child 49651 c7585f8addc2
permissions -rw-r--r--
support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm@36683
     1
/*  Title:      Pure/General/pretty.scala
wenzelm@36683
     2
    Author:     Makarius
wenzelm@36683
     3
wenzelm@36687
     4
Generic pretty printing module.
wenzelm@36683
     5
*/
wenzelm@36683
     6
wenzelm@36683
     7
package isabelle
wenzelm@36683
     8
wenzelm@36683
     9
wenzelm@36820
    10
import java.awt.FontMetrics
wenzelm@36820
    11
wenzelm@36820
    12
wenzelm@36683
    13
object Pretty
wenzelm@36683
    14
{
wenzelm@48704
    15
  /* spaces */
wenzelm@48704
    16
wenzelm@48704
    17
  val spc = ' '
wenzelm@48704
    18
  val space = " "
wenzelm@48704
    19
wenzelm@48704
    20
  private val static_spaces = space * 4000
wenzelm@48704
    21
wenzelm@48704
    22
  def spaces(k: Int): String =
wenzelm@48704
    23
  {
wenzelm@48704
    24
    require(k >= 0)
wenzelm@48704
    25
    if (k < static_spaces.length) static_spaces.substring(0, k)
wenzelm@48704
    26
    else space * k
wenzelm@48704
    27
  }
wenzelm@48704
    28
wenzelm@48704
    29
wenzelm@36687
    30
  /* markup trees with physical blocks and breaks */
wenzelm@36687
    31
wenzelm@38573
    32
  def block(body: XML.Body): XML.Tree = Block(2, body)
wenzelm@38573
    33
wenzelm@36683
    34
  object Block
wenzelm@36683
    35
  {
wenzelm@38573
    36
    def apply(i: Int, body: XML.Body): XML.Tree =
wenzelm@45666
    37
      XML.Elem(Markup(Isabelle_Markup.BLOCK, Isabelle_Markup.Indent(i)), body)
wenzelm@36683
    38
wenzelm@38573
    39
    def unapply(tree: XML.Tree): Option[(Int, XML.Body)] =
wenzelm@36683
    40
      tree match {
wenzelm@45666
    41
        case XML.Elem(Markup(Isabelle_Markup.BLOCK, Isabelle_Markup.Indent(i)), body) =>
wenzelm@45666
    42
          Some((i, body))
wenzelm@36683
    43
        case _ => None
wenzelm@36683
    44
      }
wenzelm@36683
    45
  }
wenzelm@36683
    46
wenzelm@36683
    47
  object Break
wenzelm@36683
    48
  {
wenzelm@38414
    49
    def apply(w: Int): XML.Tree =
wenzelm@45666
    50
      XML.Elem(Markup(Isabelle_Markup.BREAK, Isabelle_Markup.Width(w)),
wenzelm@48704
    51
        List(XML.Text(spaces(w))))
wenzelm@36683
    52
wenzelm@36683
    53
    def unapply(tree: XML.Tree): Option[Int] =
wenzelm@36683
    54
      tree match {
wenzelm@45666
    55
        case XML.Elem(Markup(Isabelle_Markup.BREAK, Isabelle_Markup.Width(w)), _) => Some(w)
wenzelm@36683
    56
        case _ => None
wenzelm@36683
    57
      }
wenzelm@36683
    58
  }
wenzelm@36683
    59
wenzelm@36689
    60
  val FBreak = XML.Text("\n")
wenzelm@36687
    61
wenzelm@49473
    62
  val Separator = XML.elem(Isabelle_Markup.SEPARATOR, List(FBreak))
wenzelm@49473
    63
wenzelm@36687
    64
wenzelm@36687
    65
  /* formatted output */
wenzelm@36687
    66
wenzelm@49468
    67
  def standard_format(body: XML.Body): XML.Body =
wenzelm@49468
    68
    body flatMap {
wenzelm@49650
    69
      case XML.Wrapped_Elem(markup, body1, body2) =>
wenzelm@49650
    70
        List(XML.Wrapped_Elem(markup, body1, standard_format(body)))
wenzelm@49468
    71
      case XML.Elem(markup, body) => List(XML.Elem(markup, standard_format(body)))
wenzelm@48996
    72
      case XML.Text(text) => Library.separate(FBreak, split_lines(text).map(XML.Text))
wenzelm@36689
    73
    }
wenzelm@36689
    74
wenzelm@45251
    75
  private sealed case class Text(tx: XML.Body = Nil, val pos: Double = 0.0, val nl: Int = 0)
wenzelm@36817
    76
  {
wenzelm@36817
    77
    def newline: Text = copy(tx = FBreak :: tx, pos = 0.0, nl = nl + 1)
wenzelm@36817
    78
    def string(s: String, len: Double): Text = copy(tx = XML.Text(s) :: tx, pos = pos + len)
wenzelm@48704
    79
    def blanks(wd: Int): Text = string(spaces(wd), wd.toDouble)
wenzelm@38573
    80
    def content: XML.Body = tx.reverse
wenzelm@36817
    81
  }
wenzelm@36817
    82
wenzelm@36745
    83
  private val margin_default = 76
wenzelm@36818
    84
  private def metric_default(s: String) = s.length.toDouble
wenzelm@36734
    85
wenzelm@36820
    86
  def font_metric(metrics: FontMetrics): String => Double =
wenzelm@36820
    87
    if (metrics == null) ((s: String) => s.length.toDouble)
wenzelm@36820
    88
    else {
wenzelm@48704
    89
      val unit = metrics.charWidth(spc).toDouble
wenzelm@36820
    90
      ((s: String) => if (s == "\n") 1.0 else metrics.stringWidth(s) / unit)
wenzelm@36820
    91
    }
wenzelm@36820
    92
wenzelm@38573
    93
  def formatted(input: XML.Body, margin: Int = margin_default,
wenzelm@38573
    94
    metric: String => Double = metric_default): XML.Body =
wenzelm@36687
    95
  {
wenzelm@36687
    96
    val breakgain = margin / 20
wenzelm@36687
    97
    val emergencypos = margin / 2
wenzelm@36687
    98
wenzelm@36817
    99
    def content_length(tree: XML.Tree): Double =
wenzelm@36817
   100
      tree match {
wenzelm@49650
   101
        case XML.Wrapped_Elem(_, _, body) => (0.0 /: body)(_ + content_length(_))
wenzelm@38230
   102
        case XML.Elem(_, body) => (0.0 /: body)(_ + content_length(_))
wenzelm@36817
   103
        case XML.Text(s) => metric(s)
wenzelm@36817
   104
      }
wenzelm@36817
   105
wenzelm@38573
   106
    def breakdist(trees: XML.Body, after: Double): Double =
wenzelm@36817
   107
      trees match {
wenzelm@36817
   108
        case Break(_) :: _ => 0.0
wenzelm@36817
   109
        case FBreak :: _ => 0.0
wenzelm@36818
   110
        case t :: ts => content_length(t) + breakdist(ts, after)
wenzelm@36817
   111
        case Nil => after
wenzelm@36817
   112
      }
wenzelm@36817
   113
wenzelm@38573
   114
    def forcenext(trees: XML.Body): XML.Body =
wenzelm@36817
   115
      trees match {
wenzelm@36817
   116
        case Nil => Nil
wenzelm@36817
   117
        case FBreak :: _ => trees
wenzelm@36817
   118
        case Break(_) :: ts => FBreak :: ts
wenzelm@36817
   119
        case t :: ts => t :: forcenext(ts)
wenzelm@36817
   120
      }
wenzelm@36817
   121
wenzelm@38573
   122
    def format(trees: XML.Body, blockin: Double, after: Double, text: Text): Text =
wenzelm@36687
   123
      trees match {
wenzelm@36687
   124
        case Nil => text
wenzelm@36687
   125
wenzelm@36687
   126
        case Block(indent, body) :: ts =>
wenzelm@36687
   127
          val pos1 = text.pos + indent
wenzelm@36687
   128
          val pos2 = pos1 % emergencypos
wenzelm@36687
   129
          val blockin1 =
wenzelm@36687
   130
            if (pos1 < emergencypos) pos1
wenzelm@36687
   131
            else pos2
wenzelm@36687
   132
          val btext = format(body, blockin1, breakdist(ts, after), text)
wenzelm@36687
   133
          val ts1 = if (text.nl < btext.nl) forcenext(ts) else ts
wenzelm@36687
   134
          format(ts1, blockin, after, btext)
wenzelm@36687
   135
wenzelm@36687
   136
        case Break(wd) :: ts =>
wenzelm@36687
   137
          if (text.pos + wd <= (margin - breakdist(ts, after)).max(blockin + breakgain))
wenzelm@36687
   138
            format(ts, blockin, after, text.blanks(wd))
wenzelm@36817
   139
          else format(ts, blockin, after, text.newline.blanks(blockin.toInt))
wenzelm@36817
   140
        case FBreak :: ts => format(ts, blockin, after, text.newline.blanks(blockin.toInt))
wenzelm@36687
   141
wenzelm@49650
   142
        case XML.Wrapped_Elem(markup, body1, body2) :: ts =>
wenzelm@49650
   143
          val btext = format(body2, blockin, breakdist(ts, after), text.copy(tx = Nil))
wenzelm@49650
   144
          val ts1 = if (text.nl < btext.nl) forcenext(ts) else ts
wenzelm@49650
   145
          val btext1 = btext.copy(tx = XML.Wrapped_Elem(markup, body1, btext.content) :: text.tx)
wenzelm@49650
   146
          format(ts1, blockin, after, btext1)
wenzelm@49650
   147
wenzelm@38230
   148
        case XML.Elem(markup, body) :: ts =>
wenzelm@36734
   149
          val btext = format(body, blockin, breakdist(ts, after), text.copy(tx = Nil))
wenzelm@36734
   150
          val ts1 = if (text.nl < btext.nl) forcenext(ts) else ts
wenzelm@38230
   151
          val btext1 = btext.copy(tx = XML.Elem(markup, btext.content) :: text.tx)
wenzelm@36734
   152
          format(ts1, blockin, after, btext1)
wenzelm@49650
   153
wenzelm@36817
   154
        case XML.Text(s) :: ts => format(ts, blockin, after, text.string(s, metric(s)))
wenzelm@36687
   155
      }
wenzelm@49650
   156
wenzelm@49468
   157
    format(standard_format(input), 0.0, 0.0, Text()).content
wenzelm@36687
   158
  }
wenzelm@36734
   159
wenzelm@38573
   160
  def string_of(input: XML.Body, margin: Int = margin_default,
wenzelm@36818
   161
      metric: String => Double = metric_default): String =
wenzelm@49416
   162
    XML.content(formatted(input, margin, metric))
wenzelm@36736
   163
wenzelm@36736
   164
wenzelm@36736
   165
  /* unformatted output */
wenzelm@36736
   166
wenzelm@38573
   167
  def unformatted(input: XML.Body): XML.Body =
wenzelm@36736
   168
  {
wenzelm@38573
   169
    def fmt(tree: XML.Tree): XML.Body =
wenzelm@36736
   170
      tree match {
wenzelm@36736
   171
        case Block(_, body) => body.flatMap(fmt)
wenzelm@48704
   172
        case Break(wd) => List(XML.Text(spaces(wd)))
wenzelm@48704
   173
        case FBreak => List(XML.Text(space))
wenzelm@49650
   174
        case XML.Wrapped_Elem(markup, body1, body2) =>
wenzelm@49650
   175
          List(XML.Wrapped_Elem(markup, body1, body2.flatMap(fmt)))
wenzelm@38230
   176
        case XML.Elem(markup, body) => List(XML.Elem(markup, body.flatMap(fmt)))
wenzelm@36736
   177
        case XML.Text(_) => List(tree)
wenzelm@36736
   178
      }
wenzelm@49468
   179
    standard_format(input).flatMap(fmt)
wenzelm@36736
   180
  }
wenzelm@36736
   181
wenzelm@49416
   182
  def str_of(input: XML.Body): String = XML.content(unformatted(input))
wenzelm@36683
   183
}