1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
|
use ui;
use core:io;
use core:geometry;
use graphics;
/**
* An element that renders text colored as specified.
*
* Does not do automatic word wrapping.
*/
class ColoredText extends Element {
// Font for the text.
private Font font;
// Default fill brush.
private Brush defaultBrush;
// Lines of text to draw.
private Line[] lines;
// Marked regions.
private Marked[] marked;
// Remember where labels start.
private Str->Nat labels;
// Create.
init(TextStyle style) {
init() {
font = style.font;
defaultBrush = style.fill;
}
// Start the first line.
nextLine();
}
// Add a chunk of text with the default color.
void text(Str t) {
text(t, defaultBrush);
}
// Add a chunk of text with the specified brush.
void text(Str t, Brush b) {
lines.last.add(Chunk(Text(t, font), b));
var w = lines.last.width;
for (m in marked) {
m.rect.p1.x = max(m.rect.p1.x, w);
}
}
// Add a chunk of text with the specified color.
void text(Str t, Color c) {
text(t, SolidBrush(c));
}
// Skip to the next line.
void nextLine() {
lines << Line();
}
// Begin a marked text region.
void begin(Str label) {
Nat id = lines.count;
if (id > 0) id--;
labels.put(label, id);
}
// End a marked text region.
void end(Str label, Color border, Color fill) {
Nat from = labels.get(label);
Nat to = lines.count;
Rect pos;
Float y = 0;
for (i, line in lines) {
pos.p1.x = max(pos.p1.x, line.width);
if (i == from) {
pos.p0.y = y;
}
if (i < to) {
pos.p1.y = y;
}
y += line.height;
}
marked << Marked(pos, SolidBrush(border), SolidBrush(fill));
}
// Minimum size.
Size minSize() : override {
Size total;
for (l in lines) {
total.w = max(total.w, l.width);
total.h += l.height;
}
total;
}
// Draw.
void draw(Graphics g) : override {
Point at = pos.p0;
for (m in marked) {
Rect r = m.rect + at;
g.draw(r, m.border);
if (fill = m.fill)
g.fill(r, fill);
}
for (l in lines) {
l.draw(g, at);
at.y += l.height;
}
}
// Representation of a single line.
private class Line on Render {
// Total height of the line.
Float height;
// Total width of the line.
Float width;
// Get the size.
Size size() {
Size(width, height);
}
// Individual text chunks in the line.
Chunk[] chunks;
// Add a chunk, keep the height updated.
void add(Chunk chunk) {
chunks << chunk;
Size sz = chunk.text.size;
height = max(height, sz.h);
width += sz.w;
}
// Draw!
void draw(Graphics g, Point at) {
for (c in chunks) {
Size sz = c.text.size;
g.draw(c.text, c.fill, Point(at.x, at.y + height - sz.h));
at.x += sz.w;
}
}
}
// A chunk of text.
private value Chunk {
// Text.
Text text;
// Color.
Brush fill;
// Create.
init(Text t, Brush b) {
init() { text = t; fill = b; }
}
}
// A marked region of text.
private class Marked {
// Border color.
Brush border;
// Fill color.
Brush? fill;
// Rectangle to fill.
Rect rect;
// Create.
init(Rect rect, Brush border, Brush? fill) {
init() { border = border; fill = fill; rect = rect; }
}
}
}
|
