author | wenzelm |
Fri, 24 Feb 2012 22:58:13 +0100 | |
changeset 46661 | d2ac78ba805e |
parent 45666 | d83797ef0d2d |
child 48704 | 85a3de10567d |
permissions | -rw-r--r-- |
36683 | 1 |
/* Title: Pure/General/pretty.scala |
2 |
Author: Makarius |
|
3 |
||
36687 | 4 |
Generic pretty printing module. |
36683 | 5 |
*/ |
6 |
||
7 |
package isabelle |
|
8 |
||
9 |
||
36820 | 10 |
import java.awt.FontMetrics |
11 |
||
12 |
||
36683 | 13 |
object Pretty |
14 |
{ |
|
36687 | 15 |
/* markup trees with physical blocks and breaks */ |
16 |
||
38573 | 17 |
def block(body: XML.Body): XML.Tree = Block(2, body) |
18 |
||
36683 | 19 |
object Block |
20 |
{ |
|
38573 | 21 |
def apply(i: Int, body: XML.Body): XML.Tree = |
45666 | 22 |
XML.Elem(Markup(Isabelle_Markup.BLOCK, Isabelle_Markup.Indent(i)), body) |
36683 | 23 |
|
38573 | 24 |
def unapply(tree: XML.Tree): Option[(Int, XML.Body)] = |
36683 | 25 |
tree match { |
45666 | 26 |
case XML.Elem(Markup(Isabelle_Markup.BLOCK, Isabelle_Markup.Indent(i)), body) => |
27 |
Some((i, body)) |
|
36683 | 28 |
case _ => None |
29 |
} |
|
30 |
} |
|
31 |
||
32 |
object Break |
|
33 |
{ |
|
38414
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38230
diff
changeset
|
34 |
def apply(w: Int): XML.Tree = |
45666 | 35 |
XML.Elem(Markup(Isabelle_Markup.BREAK, Isabelle_Markup.Width(w)), |
36 |
List(XML.Text(Symbol.spaces(w)))) |
|
36683 | 37 |
|
38 |
def unapply(tree: XML.Tree): Option[Int] = |
|
39 |
tree match { |
|
45666 | 40 |
case XML.Elem(Markup(Isabelle_Markup.BREAK, Isabelle_Markup.Width(w)), _) => Some(w) |
36683 | 41 |
case _ => None |
42 |
} |
|
43 |
} |
|
44 |
||
36689
379f5b1e7f91
replaced slightly odd fbreak markup by plain "\n", which also coincides with regular linebreaks produced outside the ML pretty engine;
wenzelm
parents:
36687
diff
changeset
|
45 |
val FBreak = XML.Text("\n") |
36687 | 46 |
|
47 |
||
48 |
/* formatted output */ |
|
49 |
||
38573 | 50 |
private def standard_format(tree: XML.Tree): XML.Body = |
36689
379f5b1e7f91
replaced slightly odd fbreak markup by plain "\n", which also coincides with regular linebreaks produced outside the ML pretty engine;
wenzelm
parents:
36687
diff
changeset
|
51 |
tree match { |
38230
ed147003de4b
simplified type XML.Tree: embed Markup directly, avoid slightly odd triple;
wenzelm
parents:
37374
diff
changeset
|
52 |
case XML.Elem(markup, body) => List(XML.Elem(markup, body.flatMap(standard_format))) |
36689
379f5b1e7f91
replaced slightly odd fbreak markup by plain "\n", which also coincides with regular linebreaks produced outside the ML pretty engine;
wenzelm
parents:
36687
diff
changeset
|
53 |
case XML.Text(text) => |
379f5b1e7f91
replaced slightly odd fbreak markup by plain "\n", which also coincides with regular linebreaks produced outside the ML pretty engine;
wenzelm
parents:
36687
diff
changeset
|
54 |
Library.separate(FBreak, |
379f5b1e7f91
replaced slightly odd fbreak markup by plain "\n", which also coincides with regular linebreaks produced outside the ML pretty engine;
wenzelm
parents:
36687
diff
changeset
|
55 |
Library.chunks(text).toList.map((s: CharSequence) => XML.Text(s.toString))) |
379f5b1e7f91
replaced slightly odd fbreak markup by plain "\n", which also coincides with regular linebreaks produced outside the ML pretty engine;
wenzelm
parents:
36687
diff
changeset
|
56 |
} |
379f5b1e7f91
replaced slightly odd fbreak markup by plain "\n", which also coincides with regular linebreaks produced outside the ML pretty engine;
wenzelm
parents:
36687
diff
changeset
|
57 |
|
45251 | 58 |
private sealed case class Text(tx: XML.Body = Nil, val pos: Double = 0.0, val nl: Int = 0) |
36817
ed97e877ff2d
more precise pretty printing based on actual font metrics;
wenzelm
parents:
36763
diff
changeset
|
59 |
{ |
ed97e877ff2d
more precise pretty printing based on actual font metrics;
wenzelm
parents:
36763
diff
changeset
|
60 |
def newline: Text = copy(tx = FBreak :: tx, pos = 0.0, nl = nl + 1) |
ed97e877ff2d
more precise pretty printing based on actual font metrics;
wenzelm
parents:
36763
diff
changeset
|
61 |
def string(s: String, len: Double): Text = copy(tx = XML.Text(s) :: tx, pos = pos + len) |
ed97e877ff2d
more precise pretty printing based on actual font metrics;
wenzelm
parents:
36763
diff
changeset
|
62 |
def blanks(wd: Int): Text = string(Symbol.spaces(wd), wd.toDouble) |
38573 | 63 |
def content: XML.Body = tx.reverse |
36817
ed97e877ff2d
more precise pretty printing based on actual font metrics;
wenzelm
parents:
36763
diff
changeset
|
64 |
} |
ed97e877ff2d
more precise pretty printing based on actual font metrics;
wenzelm
parents:
36763
diff
changeset
|
65 |
|
36745 | 66 |
private val margin_default = 76 |
36818 | 67 |
private def metric_default(s: String) = s.length.toDouble |
36734
d9b10c173330
Pretty.formatted operates directly on XML trees, treating XML.Elem like a pro-forma block of indentation 0, like the ML version;
wenzelm
parents:
36689
diff
changeset
|
68 |
|
36820 | 69 |
def font_metric(metrics: FontMetrics): String => Double = |
70 |
if (metrics == null) ((s: String) => s.length.toDouble) |
|
71 |
else { |
|
72 |
val unit = metrics.charWidth(Symbol.spc).toDouble |
|
73 |
((s: String) => if (s == "\n") 1.0 else metrics.stringWidth(s) / unit) |
|
74 |
} |
|
75 |
||
38573 | 76 |
def formatted(input: XML.Body, margin: Int = margin_default, |
77 |
metric: String => Double = metric_default): XML.Body = |
|
36687 | 78 |
{ |
79 |
val breakgain = margin / 20 |
|
80 |
val emergencypos = margin / 2 |
|
81 |
||
36817
ed97e877ff2d
more precise pretty printing based on actual font metrics;
wenzelm
parents:
36763
diff
changeset
|
82 |
def content_length(tree: XML.Tree): Double = |
ed97e877ff2d
more precise pretty printing based on actual font metrics;
wenzelm
parents:
36763
diff
changeset
|
83 |
tree match { |
38230
ed147003de4b
simplified type XML.Tree: embed Markup directly, avoid slightly odd triple;
wenzelm
parents:
37374
diff
changeset
|
84 |
case XML.Elem(_, body) => (0.0 /: body)(_ + content_length(_)) |
36817
ed97e877ff2d
more precise pretty printing based on actual font metrics;
wenzelm
parents:
36763
diff
changeset
|
85 |
case XML.Text(s) => metric(s) |
ed97e877ff2d
more precise pretty printing based on actual font metrics;
wenzelm
parents:
36763
diff
changeset
|
86 |
} |
ed97e877ff2d
more precise pretty printing based on actual font metrics;
wenzelm
parents:
36763
diff
changeset
|
87 |
|
38573 | 88 |
def breakdist(trees: XML.Body, after: Double): Double = |
36817
ed97e877ff2d
more precise pretty printing based on actual font metrics;
wenzelm
parents:
36763
diff
changeset
|
89 |
trees match { |
ed97e877ff2d
more precise pretty printing based on actual font metrics;
wenzelm
parents:
36763
diff
changeset
|
90 |
case Break(_) :: _ => 0.0 |
ed97e877ff2d
more precise pretty printing based on actual font metrics;
wenzelm
parents:
36763
diff
changeset
|
91 |
case FBreak :: _ => 0.0 |
36818 | 92 |
case t :: ts => content_length(t) + breakdist(ts, after) |
36817
ed97e877ff2d
more precise pretty printing based on actual font metrics;
wenzelm
parents:
36763
diff
changeset
|
93 |
case Nil => after |
ed97e877ff2d
more precise pretty printing based on actual font metrics;
wenzelm
parents:
36763
diff
changeset
|
94 |
} |
ed97e877ff2d
more precise pretty printing based on actual font metrics;
wenzelm
parents:
36763
diff
changeset
|
95 |
|
38573 | 96 |
def forcenext(trees: XML.Body): XML.Body = |
36817
ed97e877ff2d
more precise pretty printing based on actual font metrics;
wenzelm
parents:
36763
diff
changeset
|
97 |
trees match { |
ed97e877ff2d
more precise pretty printing based on actual font metrics;
wenzelm
parents:
36763
diff
changeset
|
98 |
case Nil => Nil |
ed97e877ff2d
more precise pretty printing based on actual font metrics;
wenzelm
parents:
36763
diff
changeset
|
99 |
case FBreak :: _ => trees |
ed97e877ff2d
more precise pretty printing based on actual font metrics;
wenzelm
parents:
36763
diff
changeset
|
100 |
case Break(_) :: ts => FBreak :: ts |
ed97e877ff2d
more precise pretty printing based on actual font metrics;
wenzelm
parents:
36763
diff
changeset
|
101 |
case t :: ts => t :: forcenext(ts) |
ed97e877ff2d
more precise pretty printing based on actual font metrics;
wenzelm
parents:
36763
diff
changeset
|
102 |
} |
ed97e877ff2d
more precise pretty printing based on actual font metrics;
wenzelm
parents:
36763
diff
changeset
|
103 |
|
38573 | 104 |
def format(trees: XML.Body, blockin: Double, after: Double, text: Text): Text = |
36687 | 105 |
trees match { |
106 |
case Nil => text |
|
107 |
||
108 |
case Block(indent, body) :: ts => |
|
109 |
val pos1 = text.pos + indent |
|
110 |
val pos2 = pos1 % emergencypos |
|
111 |
val blockin1 = |
|
112 |
if (pos1 < emergencypos) pos1 |
|
113 |
else pos2 |
|
114 |
val btext = format(body, blockin1, breakdist(ts, after), text) |
|
115 |
val ts1 = if (text.nl < btext.nl) forcenext(ts) else ts |
|
116 |
format(ts1, blockin, after, btext) |
|
117 |
||
118 |
case Break(wd) :: ts => |
|
119 |
if (text.pos + wd <= (margin - breakdist(ts, after)).max(blockin + breakgain)) |
|
120 |
format(ts, blockin, after, text.blanks(wd)) |
|
36817
ed97e877ff2d
more precise pretty printing based on actual font metrics;
wenzelm
parents:
36763
diff
changeset
|
121 |
else format(ts, blockin, after, text.newline.blanks(blockin.toInt)) |
ed97e877ff2d
more precise pretty printing based on actual font metrics;
wenzelm
parents:
36763
diff
changeset
|
122 |
case FBreak :: ts => format(ts, blockin, after, text.newline.blanks(blockin.toInt)) |
36687 | 123 |
|
38230
ed147003de4b
simplified type XML.Tree: embed Markup directly, avoid slightly odd triple;
wenzelm
parents:
37374
diff
changeset
|
124 |
case XML.Elem(markup, body) :: ts => |
36734
d9b10c173330
Pretty.formatted operates directly on XML trees, treating XML.Elem like a pro-forma block of indentation 0, like the ML version;
wenzelm
parents:
36689
diff
changeset
|
125 |
val btext = format(body, blockin, breakdist(ts, after), text.copy(tx = Nil)) |
d9b10c173330
Pretty.formatted operates directly on XML trees, treating XML.Elem like a pro-forma block of indentation 0, like the ML version;
wenzelm
parents:
36689
diff
changeset
|
126 |
val ts1 = if (text.nl < btext.nl) forcenext(ts) else ts |
38230
ed147003de4b
simplified type XML.Tree: embed Markup directly, avoid slightly odd triple;
wenzelm
parents:
37374
diff
changeset
|
127 |
val btext1 = btext.copy(tx = XML.Elem(markup, btext.content) :: text.tx) |
36734
d9b10c173330
Pretty.formatted operates directly on XML trees, treating XML.Elem like a pro-forma block of indentation 0, like the ML version;
wenzelm
parents:
36689
diff
changeset
|
128 |
format(ts1, blockin, after, btext1) |
36817
ed97e877ff2d
more precise pretty printing based on actual font metrics;
wenzelm
parents:
36763
diff
changeset
|
129 |
case XML.Text(s) :: ts => format(ts, blockin, after, text.string(s, metric(s))) |
36687 | 130 |
} |
36817
ed97e877ff2d
more precise pretty printing based on actual font metrics;
wenzelm
parents:
36763
diff
changeset
|
131 |
format(input.flatMap(standard_format), 0.0, 0.0, Text()).content |
36687 | 132 |
} |
36734
d9b10c173330
Pretty.formatted operates directly on XML trees, treating XML.Elem like a pro-forma block of indentation 0, like the ML version;
wenzelm
parents:
36689
diff
changeset
|
133 |
|
38573 | 134 |
def string_of(input: XML.Body, margin: Int = margin_default, |
36818 | 135 |
metric: String => Double = metric_default): String = |
37374
d66e6cc47fab
Pretty.string_of (in Scala): actually observe margin/metric;
wenzelm
parents:
36820
diff
changeset
|
136 |
formatted(input, margin, metric).iterator.flatMap(XML.content).mkString |
36736 | 137 |
|
138 |
||
139 |
/* unformatted output */ |
|
140 |
||
38573 | 141 |
def unformatted(input: XML.Body): XML.Body = |
36736 | 142 |
{ |
38573 | 143 |
def fmt(tree: XML.Tree): XML.Body = |
36736 | 144 |
tree match { |
145 |
case Block(_, body) => body.flatMap(fmt) |
|
36763 | 146 |
case Break(wd) => List(XML.Text(Symbol.spaces(wd))) |
36817
ed97e877ff2d
more precise pretty printing based on actual font metrics;
wenzelm
parents:
36763
diff
changeset
|
147 |
case FBreak => List(XML.Text(Symbol.space)) |
38230
ed147003de4b
simplified type XML.Tree: embed Markup directly, avoid slightly odd triple;
wenzelm
parents:
37374
diff
changeset
|
148 |
case XML.Elem(markup, body) => List(XML.Elem(markup, body.flatMap(fmt))) |
36736 | 149 |
case XML.Text(_) => List(tree) |
150 |
} |
|
151 |
input.flatMap(standard_format).flatMap(fmt) |
|
152 |
} |
|
153 |
||
38573 | 154 |
def str_of(input: XML.Body): String = |
36736 | 155 |
unformatted(input).iterator.flatMap(XML.content).mkString |
36683 | 156 |
} |