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