src/Pure/General/pretty.scala
author wenzelm
Mon Mar 25 10:37:38 2013 +0100 (2013-03-25)
changeset 51507 ebd5366e7a42
parent 51493 59d8a1031c00
child 51568 cdb4b7dc76cb
permissions -rw-r--r--
tuned signature;
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 space = " "
wenzelm@48704
    18
wenzelm@48704
    19
  private val static_spaces = space * 4000
wenzelm@48704
    20
wenzelm@48704
    21
  def spaces(k: Int): String =
wenzelm@48704
    22
  {
wenzelm@48704
    23
    require(k >= 0)
wenzelm@48704
    24
    if (k < static_spaces.length) static_spaces.substring(0, k)
wenzelm@48704
    25
    else space * k
wenzelm@48704
    26
  }
wenzelm@48704
    27
wenzelm@48704
    28
wenzelm@51492
    29
  /* text metric -- standardized to width of space */
wenzelm@51492
    30
wenzelm@51492
    31
  abstract class Metric
wenzelm@51492
    32
  {
wenzelm@51492
    33
    val unit: Double
wenzelm@51492
    34
    def apply(s: String): Double
wenzelm@51492
    35
  }
wenzelm@51492
    36
wenzelm@51492
    37
  object Metric_Default extends Metric
wenzelm@51492
    38
  {
wenzelm@51492
    39
    val unit = 1.0
wenzelm@51492
    40
    def apply(s: String): Double = s.length.toDouble
wenzelm@51492
    41
  }
wenzelm@51492
    42
wenzelm@51492
    43
wenzelm@36687
    44
  /* markup trees with physical blocks and breaks */
wenzelm@36687
    45
wenzelm@38573
    46
  def block(body: XML.Body): XML.Tree = Block(2, body)
wenzelm@38573
    47
wenzelm@36683
    48
  object Block
wenzelm@36683
    49
  {
wenzelm@38573
    50
    def apply(i: Int, body: XML.Body): XML.Tree =
wenzelm@50201
    51
      XML.Elem(Markup(Markup.BLOCK, Markup.Indent(i)), body)
wenzelm@36683
    52
wenzelm@38573
    53
    def unapply(tree: XML.Tree): Option[(Int, XML.Body)] =
wenzelm@36683
    54
      tree match {
wenzelm@50201
    55
        case XML.Elem(Markup(Markup.BLOCK, Markup.Indent(i)), body) =>
wenzelm@45666
    56
          Some((i, body))
wenzelm@36683
    57
        case _ => None
wenzelm@36683
    58
      }
wenzelm@36683
    59
  }
wenzelm@36683
    60
wenzelm@36683
    61
  object Break
wenzelm@36683
    62
  {
wenzelm@38414
    63
    def apply(w: Int): XML.Tree =
wenzelm@50201
    64
      XML.Elem(Markup(Markup.BREAK, Markup.Width(w)),
wenzelm@48704
    65
        List(XML.Text(spaces(w))))
wenzelm@36683
    66
wenzelm@36683
    67
    def unapply(tree: XML.Tree): Option[Int] =
wenzelm@36683
    68
      tree match {
wenzelm@50201
    69
        case XML.Elem(Markup(Markup.BREAK, Markup.Width(w)), _) => Some(w)
wenzelm@36683
    70
        case _ => None
wenzelm@36683
    71
      }
wenzelm@36683
    72
  }
wenzelm@36683
    73
wenzelm@36689
    74
  val FBreak = XML.Text("\n")
wenzelm@36687
    75
wenzelm@50201
    76
  val Separator = List(XML.elem(Markup.SEPARATOR, List(XML.Text(space))), FBreak)
wenzelm@49843
    77
  def separate(ts: List[XML.Tree]): XML.Body = Library.separate(Separator, ts.map(List(_))).flatten
wenzelm@49473
    78
wenzelm@36687
    79
wenzelm@36687
    80
  /* formatted output */
wenzelm@36687
    81
wenzelm@49468
    82
  def standard_format(body: XML.Body): XML.Body =
wenzelm@49468
    83
    body flatMap {
wenzelm@49650
    84
      case XML.Wrapped_Elem(markup, body1, body2) =>
wenzelm@49657
    85
        List(XML.Wrapped_Elem(markup, body1, standard_format(body2)))
wenzelm@49468
    86
      case XML.Elem(markup, body) => List(XML.Elem(markup, standard_format(body)))
wenzelm@48996
    87
      case XML.Text(text) => Library.separate(FBreak, split_lines(text).map(XML.Text))
wenzelm@36689
    88
    }
wenzelm@36689
    89
wenzelm@51493
    90
  private val margin_default = 76.0
wenzelm@36820
    91
wenzelm@51493
    92
  def formatted(input: XML.Body, margin: Double = margin_default,
wenzelm@51492
    93
    metric: Metric = Metric_Default): XML.Body =
wenzelm@36687
    94
  {
wenzelm@51470
    95
    sealed case class Text(tx: XML.Body = Nil, val pos: Double = 0.0, val nl: Int = 0)
wenzelm@51470
    96
    {
wenzelm@51470
    97
      def newline: Text = copy(tx = FBreak :: tx, pos = 0.0, nl = nl + 1)
wenzelm@51492
    98
      def string(s: String): Text = copy(tx = XML.Text(s) :: tx, pos = pos + metric(s))
wenzelm@51492
    99
      def blanks(wd: Int): Text = string(spaces(wd))
wenzelm@51470
   100
      def content: XML.Body = tx.reverse
wenzelm@51470
   101
    }
wenzelm@51470
   102
wenzelm@36687
   103
    val breakgain = margin / 20
wenzelm@36687
   104
    val emergencypos = margin / 2
wenzelm@36687
   105
wenzelm@36817
   106
    def content_length(tree: XML.Tree): Double =
wenzelm@49651
   107
      XML.traverse_text(List(tree))(0.0)(_ + metric(_))
wenzelm@36817
   108
wenzelm@38573
   109
    def breakdist(trees: XML.Body, after: Double): Double =
wenzelm@36817
   110
      trees match {
wenzelm@36817
   111
        case Break(_) :: _ => 0.0
wenzelm@36817
   112
        case FBreak :: _ => 0.0
wenzelm@36818
   113
        case t :: ts => content_length(t) + breakdist(ts, after)
wenzelm@36817
   114
        case Nil => after
wenzelm@36817
   115
      }
wenzelm@36817
   116
wenzelm@38573
   117
    def forcenext(trees: XML.Body): XML.Body =
wenzelm@36817
   118
      trees match {
wenzelm@36817
   119
        case Nil => Nil
wenzelm@36817
   120
        case FBreak :: _ => trees
wenzelm@36817
   121
        case Break(_) :: ts => FBreak :: ts
wenzelm@36817
   122
        case t :: ts => t :: forcenext(ts)
wenzelm@36817
   123
      }
wenzelm@36817
   124
wenzelm@38573
   125
    def format(trees: XML.Body, blockin: Double, after: Double, text: Text): Text =
wenzelm@36687
   126
      trees match {
wenzelm@36687
   127
        case Nil => text
wenzelm@36687
   128
wenzelm@36687
   129
        case Block(indent, body) :: ts =>
wenzelm@36687
   130
          val pos1 = text.pos + indent
wenzelm@36687
   131
          val pos2 = pos1 % emergencypos
wenzelm@36687
   132
          val blockin1 =
wenzelm@36687
   133
            if (pos1 < emergencypos) pos1
wenzelm@36687
   134
            else pos2
wenzelm@36687
   135
          val btext = format(body, blockin1, breakdist(ts, after), text)
wenzelm@36687
   136
          val ts1 = if (text.nl < btext.nl) forcenext(ts) else ts
wenzelm@36687
   137
          format(ts1, blockin, after, btext)
wenzelm@36687
   138
wenzelm@36687
   139
        case Break(wd) :: ts =>
wenzelm@36687
   140
          if (text.pos + wd <= (margin - breakdist(ts, after)).max(blockin + breakgain))
wenzelm@36687
   141
            format(ts, blockin, after, text.blanks(wd))
wenzelm@36817
   142
          else format(ts, blockin, after, text.newline.blanks(blockin.toInt))
wenzelm@36817
   143
        case FBreak :: ts => format(ts, blockin, after, text.newline.blanks(blockin.toInt))
wenzelm@36687
   144
wenzelm@49650
   145
        case XML.Wrapped_Elem(markup, body1, body2) :: ts =>
wenzelm@49650
   146
          val btext = format(body2, blockin, breakdist(ts, after), text.copy(tx = Nil))
wenzelm@49650
   147
          val ts1 = if (text.nl < btext.nl) forcenext(ts) else ts
wenzelm@49650
   148
          val btext1 = btext.copy(tx = XML.Wrapped_Elem(markup, body1, btext.content) :: text.tx)
wenzelm@49650
   149
          format(ts1, blockin, after, btext1)
wenzelm@49650
   150
wenzelm@38230
   151
        case XML.Elem(markup, body) :: ts =>
wenzelm@36734
   152
          val btext = format(body, blockin, breakdist(ts, after), text.copy(tx = Nil))
wenzelm@36734
   153
          val ts1 = if (text.nl < btext.nl) forcenext(ts) else ts
wenzelm@38230
   154
          val btext1 = btext.copy(tx = XML.Elem(markup, btext.content) :: text.tx)
wenzelm@36734
   155
          format(ts1, blockin, after, btext1)
wenzelm@49650
   156
wenzelm@51492
   157
        case XML.Text(s) :: ts => format(ts, blockin, after, text.string(s))
wenzelm@36687
   158
      }
wenzelm@49650
   159
wenzelm@49468
   160
    format(standard_format(input), 0.0, 0.0, Text()).content
wenzelm@36687
   161
  }
wenzelm@36734
   162
wenzelm@51493
   163
  def string_of(input: XML.Body, margin: Double = margin_default,
wenzelm@51492
   164
      metric: Metric = Metric_Default): String =
wenzelm@49416
   165
    XML.content(formatted(input, margin, metric))
wenzelm@36736
   166
wenzelm@36736
   167
wenzelm@36736
   168
  /* unformatted output */
wenzelm@36736
   169
wenzelm@38573
   170
  def unformatted(input: XML.Body): XML.Body =
wenzelm@36736
   171
  {
wenzelm@38573
   172
    def fmt(tree: XML.Tree): XML.Body =
wenzelm@36736
   173
      tree match {
wenzelm@36736
   174
        case Block(_, body) => body.flatMap(fmt)
wenzelm@48704
   175
        case Break(wd) => List(XML.Text(spaces(wd)))
wenzelm@48704
   176
        case FBreak => List(XML.Text(space))
wenzelm@49650
   177
        case XML.Wrapped_Elem(markup, body1, body2) =>
wenzelm@49650
   178
          List(XML.Wrapped_Elem(markup, body1, body2.flatMap(fmt)))
wenzelm@38230
   179
        case XML.Elem(markup, body) => List(XML.Elem(markup, body.flatMap(fmt)))
wenzelm@36736
   180
        case XML.Text(_) => List(tree)
wenzelm@36736
   181
      }
wenzelm@49468
   182
    standard_format(input).flatMap(fmt)
wenzelm@36736
   183
  }
wenzelm@36736
   184
wenzelm@49416
   185
  def str_of(input: XML.Body): String = XML.content(unformatted(input))
wenzelm@36683
   186
}