author | wenzelm |
Sun, 09 May 2010 13:12:22 +0200 | |
changeset 36763 | 096ebe74aeaf |
parent 36745 | 403585a89772 |
child 36817 | ed97e877ff2d |
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 case class Text(tx: List[XML.Tree] = Nil, val pos: Int = 0, val nl: Int = 0) |
36687 | 49 |
{ |
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 |
def newline: Text = copy(tx = FBreak :: tx, pos = 0, nl = nl + 1) |
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
|
51 |
def string(s: String): Text = copy(tx = XML.Text(s) :: tx, pos = pos + s.length) |
36763 | 52 |
def blanks(wd: Int): Text = string(Symbol.spaces(wd)) |
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
|
53 |
def content: List[XML.Tree] = tx.reverse |
36687 | 54 |
} |
55 |
||
56 |
private def breakdist(trees: List[XML.Tree], after: Int): Int = |
|
57 |
trees match { |
|
58 |
case Break(_) :: _ => 0 |
|
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
|
59 |
case FBreak :: _ => 0 |
36687 | 60 |
case XML.Elem(_, _, body) :: ts => |
61 |
(0 /: body)(_ + XML.content_length(_)) + breakdist(ts, after) |
|
62 |
case XML.Text(s) :: ts => s.length + breakdist(ts, after) |
|
63 |
case Nil => after |
|
64 |
} |
|
65 |
||
66 |
private def forcenext(trees: List[XML.Tree]): List[XML.Tree] = |
|
67 |
trees match { |
|
68 |
case Nil => Nil |
|
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
|
69 |
case FBreak :: _ => trees |
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
|
70 |
case Break(_) :: ts => FBreak :: ts |
36687 | 71 |
case t :: ts => t :: forcenext(ts) |
72 |
} |
|
73 |
||
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
|
74 |
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
|
75 |
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
|
76 |
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
|
77 |
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
|
78 |
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
|
79 |
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
|
80 |
} |
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
|
81 |
|
36745 | 82 |
private val margin_default = 76 |
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
|
83 |
|
36745 | 84 |
def formatted(input: List[XML.Tree], margin: Int = margin_default): List[XML.Tree] = |
36687 | 85 |
{ |
86 |
val breakgain = margin / 20 |
|
87 |
val emergencypos = margin / 2 |
|
88 |
||
89 |
def format(trees: List[XML.Tree], blockin: Int, after: Int, text: Text): Text = |
|
90 |
trees match { |
|
91 |
case Nil => text |
|
92 |
||
93 |
case Block(indent, body) :: ts => |
|
94 |
val pos1 = text.pos + indent |
|
95 |
val pos2 = pos1 % emergencypos |
|
96 |
val blockin1 = |
|
97 |
if (pos1 < emergencypos) pos1 |
|
98 |
else pos2 |
|
99 |
val btext = format(body, blockin1, breakdist(ts, after), text) |
|
100 |
val ts1 = if (text.nl < btext.nl) forcenext(ts) else ts |
|
101 |
format(ts1, blockin, after, btext) |
|
102 |
||
103 |
case Break(wd) :: ts => |
|
104 |
if (text.pos + wd <= (margin - breakdist(ts, after)).max(blockin + breakgain)) |
|
105 |
format(ts, blockin, after, text.blanks(wd)) |
|
106 |
else format(ts, blockin, after, text.newline.blanks(blockin)) |
|
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
|
107 |
case FBreak :: ts => format(ts, blockin, after, text.newline.blanks(blockin)) |
36687 | 108 |
|
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
|
109 |
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
|
110 |
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
|
111 |
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
|
112 |
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
|
113 |
format(ts1, blockin, after, btext1) |
36687 | 114 |
case XML.Text(s) :: ts => format(ts, blockin, after, text.string(s)) |
115 |
} |
|
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
|
116 |
format(input.flatMap(standard_format), 0, 0, Text()).content |
36687 | 117 |
} |
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
|
118 |
|
36745 | 119 |
def string_of(input: List[XML.Tree], margin: Int = margin_default): String = |
36736 | 120 |
formatted(input).iterator.flatMap(XML.content).mkString |
121 |
||
122 |
||
123 |
/* unformatted output */ |
|
124 |
||
125 |
def unformatted(input: List[XML.Tree]): List[XML.Tree] = |
|
126 |
{ |
|
127 |
def fmt(tree: XML.Tree): List[XML.Tree] = |
|
128 |
tree match { |
|
129 |
case Block(_, body) => body.flatMap(fmt) |
|
36763 | 130 |
case Break(wd) => List(XML.Text(Symbol.spaces(wd))) |
36736 | 131 |
case FBreak => List(XML.Text(" ")) |
132 |
case XML.Elem(name, atts, body) => List(XML.Elem(name, atts, body.flatMap(fmt))) |
|
133 |
case XML.Text(_) => List(tree) |
|
134 |
} |
|
135 |
input.flatMap(standard_format).flatMap(fmt) |
|
136 |
} |
|
137 |
||
138 |
def str_of(input: List[XML.Tree]): String = |
|
139 |
unformatted(input).iterator.flatMap(XML.content).mkString |
|
36683 | 140 |
} |