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