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