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
|
use ui;
use graphics;
use core:io;
use core:lang;
use core:geometry;
use progvis:program;
class SourceView on Render {
// Program context.
Program? program;
// Current file.
Url file;
// Current text object being rendered.
Text? text;
// Where to fill at the moment.
Rect[] fill;
// Bounds of the fill area. We try to center this in the source view.
Rect fillBounds;
// Brush used to highlight.
Brush highlight;
// Brush used for text.
Brush textFg;
// Create, will try to load source code by itself.
init() {
init {
highlight = sourceHighlight;
textFg = dataFg;
}
}
// Create.
init(Program program) {
init {
program = program;
highlight = sourceHighlight;
textFg = dataFg;
}
}
// Switch to a new view.
void display(SrcPos pos) {
if (file = pos.file) {
display(file, pos.start, pos.end);
}
}
// Switch to an empty view.
void displayEmpty(Str message) {
file = Url();
Text t(message, codeFont);
text = t;
fillBounds = Rect(Point(), t.size);
fill = [fillBounds];
}
void displayEmpty() {
displayEmpty("<no source available>");
}
// Switch to a new view.
void display(Url file, Nat from, Nat to) {
if (file != this.file) {
if (program) {
text = program.source(file);
} else {
text = highlightSource(file);
}
this.file = file;
}
if (text) {
var begin = text.text.begin + from;
var end = text.text.begin + to;
fill = text.boundsOf(begin, end);
if (fill.any)
fillBounds = fill[0];
for (Nat i = 1; i < fill.count; i++) {
fillBounds = fillBounds.include(fill[i]);
}
} else {
fill = [];
// We don't re-set the bounds to prevent scrolling.
}
}
// Draw.
void draw(Graphics g, Rect pos) {
g.draw(pos, dataFg);
if (text) {
pos = pos.shrink(dataBorder);
g.push(pos);
Size size = pos.size;
Size boundsSize = fillBounds.size;
Float yOffset = pos.p0.y - fillBounds.p0.y + (size.h - boundsSize.h) / 2;
Float xOffset = max(0.0, size.w - boundsSize.w); // Where to keep the left point of the highlight.
xOffset = pos.p0.x + min(0.0, xOffset - fillBounds.p0.x);
Point offset(xOffset, yOffset);
for (f in fill) {
g.fill(f + offset, highlight);
}
g.draw(text, textFg, offset);
g.pop();
}
}
}
|
