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