text.anubis
3.21 KB
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
The Anubis/Paradize Project.
The text widget.
Copyright (c) Alain Prouté 2004-2005.
Authors: Alain Prouté
Olivier Duvernois
This widget shows a simple 'inert' text. For a more sophisticated widget see
'widgets3/hypertext.anubis'.
read widget.anubis
read tools.anubis
public define Widget
create_text
(
String text, // text to be printed (may have several lines)
SystemFont font,
RGB foreground_color,
Int32 margin // to be put on 4 sides
).
--- That's all for the public part ! --------------------------------------------------
define One
redraw_text
(
WidgetDrawToolBox dtb,
List(String) text,
SystemFont font,
Int32 total_font_height,
RGB foreground_color,
Int32 margin,
Int32 y
) =
if text is
{
[ ] then unique,
[line1 . lines] then
forget(draw(dtb)(line1,font,foreground_color,position(margin,y)));
redraw_text(dtb,
lines,
font,
total_font_height,
foreground_color,
margin,
y+total_font_height)
}.
public define Widget
create_text
(
String text, // text to be printed (may have several lines)
SystemFont font,
RGB foreground_color,
Int32 margin // to be put on 4 sides
) =
with lines = split_string_into_lines(text),
margin_twice = margin*2,
w_width = margin_twice+printed_text_width(font,lines),
w_height = margin_twice+printed_text_height(font,lines),
info = get_font_info(font),
font_height = int8_to_int32(height(info)),
font_depth = int8_to_int32(depth(info)),
total_font_height = font_height+font_depth,
create_widget
(
/* setting childs positions */
(WidgetPositionToolBox ptb) |-> unique,
/* getting size */
(One u) |-> (w_width,w_height),
/* redraw */
(WidgetDrawToolBox dtb) |->
redraw_text(dtb,
lines,
font,
total_font_height,
foreground_color,
margin,
font_height+margin),
/* duplicate */
(One u) |-> create_text(text,font,foreground_color,margin),
/* Change size */
(Int32 w, Int32 h) |-> unique,
/* main event handler */
(WidgetEventToolBox etb, WidgetNormalEvent e) |-> not_handled([]),
/* registrations */
[ ]
).