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