1 /* Title: Pure/General/pretty.scala |
1 /* Title: Pure/General/pretty.scala |
2 Author: Makarius |
2 Author: Makarius |
3 |
3 |
4 Symbolic pretty printing. |
4 Generic pretty printing module. |
5 */ |
5 */ |
6 |
6 |
7 package isabelle |
7 package isabelle |
8 |
8 |
9 |
9 |
10 object Pretty |
10 object Pretty |
11 { |
11 { |
|
12 /* markup trees with physical blocks and breaks */ |
|
13 |
12 object Block |
14 object Block |
13 { |
15 { |
14 def apply(indent: Int, body: List[XML.Tree]): XML.Tree = |
16 def apply(indent: Int, body: List[XML.Tree]): XML.Tree = |
15 XML.Elem(Markup.BLOCK, List((Markup.INDENT, indent.toString)), body) |
17 XML.Elem(Markup.BLOCK, List((Markup.INDENT, indent.toString)), body) |
16 |
18 |
45 tree match { |
47 tree match { |
46 case XML.Elem(Markup.FBREAK, Nil, _) => true |
48 case XML.Elem(Markup.FBREAK, Nil, _) => true |
47 case _ => false |
49 case _ => false |
48 } |
50 } |
49 } |
51 } |
|
52 |
|
53 |
|
54 /* formatted output */ |
|
55 |
|
56 private case class Text(tx: List[String] = Nil, val pos: Int = 0, val nl: Int = 0) |
|
57 { |
|
58 def newline: Text = copy(tx = "\n" :: tx, pos = 0, nl = nl + 1) |
|
59 def string(s: String): Text = copy(tx = s :: tx, pos = pos + s.length) |
|
60 def blanks(wd: Int): Text = string(" " * wd) |
|
61 def content: String = tx.reverse.mkString |
|
62 } |
|
63 |
|
64 private def breakdist(trees: List[XML.Tree], after: Int): Int = |
|
65 trees match { |
|
66 case Break(_) :: _ => 0 |
|
67 case FBreak() :: _ => 0 |
|
68 case XML.Elem(_, _, body) :: ts => |
|
69 (0 /: body)(_ + XML.content_length(_)) + breakdist(ts, after) |
|
70 case XML.Text(s) :: ts => s.length + breakdist(ts, after) |
|
71 case Nil => after |
|
72 } |
|
73 |
|
74 private def forcenext(trees: List[XML.Tree]): List[XML.Tree] = |
|
75 trees match { |
|
76 case Nil => Nil |
|
77 case FBreak() :: _ => trees |
|
78 case Break(_) :: ts => FBreak() :: ts |
|
79 case t :: ts => t :: forcenext(ts) |
|
80 } |
|
81 |
|
82 def string_of(input: List[XML.Tree], margin: Int = 76): String = |
|
83 { |
|
84 val breakgain = margin / 20 |
|
85 val emergencypos = margin / 2 |
|
86 |
|
87 def format(trees: List[XML.Tree], blockin: Int, after: Int, text: Text): Text = |
|
88 trees match { |
|
89 case Nil => text |
|
90 |
|
91 case Block(indent, body) :: ts => |
|
92 val pos1 = text.pos + indent |
|
93 val pos2 = pos1 % emergencypos |
|
94 val blockin1 = |
|
95 if (pos1 < emergencypos) pos1 |
|
96 else pos2 |
|
97 val btext = format(body, blockin1, breakdist(ts, after), text) |
|
98 val ts1 = if (text.nl < btext.nl) forcenext(ts) else ts |
|
99 format(ts1, blockin, after, btext) |
|
100 |
|
101 case Break(wd) :: ts => |
|
102 if (text.pos + wd <= (margin - breakdist(ts, after)).max(blockin + breakgain)) |
|
103 format(ts, blockin, after, text.blanks(wd)) |
|
104 else format(ts, blockin, after, text.newline.blanks(blockin)) |
|
105 case FBreak() :: ts => format(ts, blockin, after, text.newline.blanks(blockin)) |
|
106 |
|
107 case XML.Elem(_, _, body) :: ts => format(body ::: ts, blockin, after, text) |
|
108 case XML.Text(s) :: ts => format(ts, blockin, after, text.string(s)) |
|
109 } |
|
110 format(input, 0, 0, Text()).content |
|
111 } |
50 } |
112 } |