author | wenzelm |
Wed, 12 May 2010 11:28:52 +0200 | |
changeset 36818 | 599466689412 |
parent 36817 | ed97e877ff2d |
child 36820 | 0cdfce0bf956 |
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 |
||
10 |
object Pretty |
|
11 |
{ |
|
36687 | 12 |
/* markup trees with physical blocks and breaks */ |
13 |
||
36683 | 14 |
object Block |
15 |
{ |
|
16 |
def apply(indent: Int, body: List[XML.Tree]): XML.Tree = |
|
17 |
XML.Elem(Markup.BLOCK, List((Markup.INDENT, indent.toString)), body) |
|
18 |
||
19 |
def unapply(tree: XML.Tree): Option[(Int, List[XML.Tree])] = |
|
20 |
tree match { |
|
21 |
case XML.Elem(Markup.BLOCK, List((Markup.INDENT, indent)), body) => |
|
22 |
Markup.parse_int(indent) match { |
|
23 |
case Some(i) => Some((i, body)) |
|
24 |
case None => None |
|
25 |
} |
|
26 |
case _ => None |
|
27 |
} |
|
28 |
} |
|
29 |
||
30 |
object Break |
|
31 |
{ |
|
32 |
def apply(width: Int): XML.Tree = |
|
36763 | 33 |
XML.Elem(Markup.BREAK, List((Markup.WIDTH, width.toString)), |
34 |
List(XML.Text(Symbol.spaces(width)))) |
|
36683 | 35 |
|
36 |
def unapply(tree: XML.Tree): Option[Int] = |
|
37 |
tree match { |
|
38 |
case XML.Elem(Markup.BREAK, List((Markup.WIDTH, width)), _) => Markup.parse_int(width) |
|
39 |
case _ => None |
|
40 |
} |
|
41 |
} |
|
42 |
||
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
|
43 |
val FBreak = XML.Text("\n") |
36687 | 44 |
|
45 |
||
46 |
/* formatted output */ |
|
47 |
||
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
|
48 |
private def standard_format(tree: XML.Tree): List[XML.Tree] = |
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
|
49 |
tree match { |
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
|
50 |
case XML.Elem(name, atts, body) => List(XML.Elem(name, atts, 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
|
51 |
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
|
52 |
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
|
53 |
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
|
54 |
} |
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 |
|
36817
ed97e877ff2d
more precise pretty printing based on actual font metrics;
wenzelm
parents:
36763
diff
changeset
|
56 |
case class Text(tx: List[XML.Tree] = Nil, val pos: Double = 0.0, val nl: Int = 0) |
ed97e877ff2d
more precise pretty printing based on actual font metrics;
wenzelm
parents:
36763
diff
changeset
|
57 |
{ |
ed97e877ff2d
more precise pretty printing based on actual font metrics;
wenzelm
parents:
36763
diff
changeset
|
58 |
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
|
59 |
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
|
60 |
def blanks(wd: Int): Text = string(Symbol.spaces(wd), wd.toDouble) |
ed97e877ff2d
more precise pretty printing based on actual font metrics;
wenzelm
parents:
36763
diff
changeset
|
61 |
def content: List[XML.Tree] = tx.reverse |
ed97e877ff2d
more precise pretty printing based on actual font metrics;
wenzelm
parents:
36763
diff
changeset
|
62 |
} |
ed97e877ff2d
more precise pretty printing based on actual font metrics;
wenzelm
parents:
36763
diff
changeset
|
63 |
|
36745 | 64 |
private val margin_default = 76 |
36818 | 65 |
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
|
66 |
|
36817
ed97e877ff2d
more precise pretty printing based on actual font metrics;
wenzelm
parents:
36763
diff
changeset
|
67 |
def formatted(input: List[XML.Tree], margin: Int = margin_default, |
36818 | 68 |
metric: String => Double = metric_default): List[XML.Tree] = |
36687 | 69 |
{ |
70 |
val breakgain = margin / 20 |
|
71 |
val emergencypos = margin / 2 |
|
72 |
||
36817
ed97e877ff2d
more precise pretty printing based on actual font metrics;
wenzelm
parents:
36763
diff
changeset
|
73 |
def content_length(tree: XML.Tree): Double = |
ed97e877ff2d
more precise pretty printing based on actual font metrics;
wenzelm
parents:
36763
diff
changeset
|
74 |
tree match { |
ed97e877ff2d
more precise pretty printing based on actual font metrics;
wenzelm
parents:
36763
diff
changeset
|
75 |
case XML.Elem(_, _, body) => (0.0 /: body)(_ + content_length(_)) |
ed97e877ff2d
more precise pretty printing based on actual font metrics;
wenzelm
parents:
36763
diff
changeset
|
76 |
case XML.Text(s) => metric(s) |
ed97e877ff2d
more precise pretty printing based on actual font metrics;
wenzelm
parents:
36763
diff
changeset
|
77 |
} |
ed97e877ff2d
more precise pretty printing based on actual font metrics;
wenzelm
parents:
36763
diff
changeset
|
78 |
|
ed97e877ff2d
more precise pretty printing based on actual font metrics;
wenzelm
parents:
36763
diff
changeset
|
79 |
def breakdist(trees: List[XML.Tree], after: Double): Double = |
ed97e877ff2d
more precise pretty printing based on actual font metrics;
wenzelm
parents:
36763
diff
changeset
|
80 |
trees match { |
ed97e877ff2d
more precise pretty printing based on actual font metrics;
wenzelm
parents:
36763
diff
changeset
|
81 |
case Break(_) :: _ => 0.0 |
ed97e877ff2d
more precise pretty printing based on actual font metrics;
wenzelm
parents:
36763
diff
changeset
|
82 |
case FBreak :: _ => 0.0 |
36818 | 83 |
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
|
84 |
case Nil => after |
ed97e877ff2d
more precise pretty printing based on actual font metrics;
wenzelm
parents:
36763
diff
changeset
|
85 |
} |
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 |
def forcenext(trees: List[XML.Tree]): List[XML.Tree] = |
ed97e877ff2d
more precise pretty printing based on actual font metrics;
wenzelm
parents:
36763
diff
changeset
|
88 |
trees match { |
ed97e877ff2d
more precise pretty printing based on actual font metrics;
wenzelm
parents:
36763
diff
changeset
|
89 |
case Nil => Nil |
ed97e877ff2d
more precise pretty printing based on actual font metrics;
wenzelm
parents:
36763
diff
changeset
|
90 |
case FBreak :: _ => trees |
ed97e877ff2d
more precise pretty printing based on actual font metrics;
wenzelm
parents:
36763
diff
changeset
|
91 |
case Break(_) :: ts => FBreak :: ts |
ed97e877ff2d
more precise pretty printing based on actual font metrics;
wenzelm
parents:
36763
diff
changeset
|
92 |
case t :: ts => t :: forcenext(ts) |
ed97e877ff2d
more precise pretty printing based on actual font metrics;
wenzelm
parents:
36763
diff
changeset
|
93 |
} |
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 |
def format(trees: List[XML.Tree], blockin: Double, after: Double, text: Text): Text = |
36687 | 96 |
trees match { |
97 |
case Nil => text |
|
98 |
||
99 |
case Block(indent, body) :: ts => |
|
100 |
val pos1 = text.pos + indent |
|
101 |
val pos2 = pos1 % emergencypos |
|
102 |
val blockin1 = |
|
103 |
if (pos1 < emergencypos) pos1 |
|
104 |
else pos2 |
|
105 |
val btext = format(body, blockin1, breakdist(ts, after), text) |
|
106 |
val ts1 = if (text.nl < btext.nl) forcenext(ts) else ts |
|
107 |
format(ts1, blockin, after, btext) |
|
108 |
||
109 |
case Break(wd) :: ts => |
|
110 |
if (text.pos + wd <= (margin - breakdist(ts, after)).max(blockin + breakgain)) |
|
111 |
format(ts, blockin, after, text.blanks(wd)) |
|
36817
ed97e877ff2d
more precise pretty printing based on actual font metrics;
wenzelm
parents:
36763
diff
changeset
|
112 |
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
|
113 |
case FBreak :: ts => format(ts, blockin, after, text.newline.blanks(blockin.toInt)) |
36687 | 114 |
|
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
|
115 |
case XML.Elem(name, atts, body) :: ts => |
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
|
116 |
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
|
117 |
val ts1 = if (text.nl < btext.nl) forcenext(ts) else ts |
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
|
118 |
val btext1 = btext.copy(tx = XML.Elem(name, atts, btext.content) :: text.tx) |
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
|
119 |
format(ts1, blockin, after, btext1) |
36817
ed97e877ff2d
more precise pretty printing based on actual font metrics;
wenzelm
parents:
36763
diff
changeset
|
120 |
case XML.Text(s) :: ts => format(ts, blockin, after, text.string(s, metric(s))) |
36687 | 121 |
} |
36817
ed97e877ff2d
more precise pretty printing based on actual font metrics;
wenzelm
parents:
36763
diff
changeset
|
122 |
format(input.flatMap(standard_format), 0.0, 0.0, Text()).content |
36687 | 123 |
} |
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
|
124 |
|
36818 | 125 |
def string_of(input: List[XML.Tree], margin: Int = margin_default, |
126 |
metric: String => Double = metric_default): String = |
|
36736 | 127 |
formatted(input).iterator.flatMap(XML.content).mkString |
128 |
||
129 |
||
130 |
/* unformatted output */ |
|
131 |
||
132 |
def unformatted(input: List[XML.Tree]): List[XML.Tree] = |
|
133 |
{ |
|
134 |
def fmt(tree: XML.Tree): List[XML.Tree] = |
|
135 |
tree match { |
|
136 |
case Block(_, body) => body.flatMap(fmt) |
|
36763 | 137 |
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
|
138 |
case FBreak => List(XML.Text(Symbol.space)) |
36736 | 139 |
case XML.Elem(name, atts, body) => List(XML.Elem(name, atts, body.flatMap(fmt))) |
140 |
case XML.Text(_) => List(tree) |
|
141 |
} |
|
142 |
input.flatMap(standard_format).flatMap(fmt) |
|
143 |
} |
|
144 |
||
145 |
def str_of(input: List[XML.Tree]): String = |
|
146 |
unformatted(input).iterator.flatMap(XML.content).mkString |
|
36683 | 147 |
} |