33823
|
1 |
(* Title: Tools/WWW_Find/xhtml.ML
|
33817
|
2 |
Author: Timothy Bourke, NICTA
|
|
3 |
|
|
4 |
Rudimentary XHTML construction.
|
|
5 |
*)
|
33823
|
6 |
|
33817
|
7 |
signature XHTML =
|
|
8 |
sig
|
|
9 |
type attribute
|
|
10 |
type common_atts = { id : string option,
|
|
11 |
class : string option };
|
|
12 |
val noid : common_atts;
|
|
13 |
val id : string -> common_atts;
|
|
14 |
val class : string -> common_atts;
|
|
15 |
|
|
16 |
type tag
|
|
17 |
|
|
18 |
val doctype_xhtml1_0_strict: string;
|
|
19 |
|
|
20 |
val att: string -> string -> attribute
|
|
21 |
val bool_att: string * bool -> attribute list
|
|
22 |
|
|
23 |
val tag: string -> attribute list -> tag list -> tag
|
|
24 |
val tag': string -> common_atts -> tag list -> tag
|
|
25 |
val text: string -> tag
|
|
26 |
val raw_text: string -> tag
|
|
27 |
|
|
28 |
val add_attributes: attribute list -> tag -> tag
|
|
29 |
val append: tag -> tag list -> tag
|
|
30 |
|
|
31 |
val show: tag -> string list
|
|
32 |
|
|
33 |
val write: (string -> unit) -> tag -> unit
|
|
34 |
val write_open: (string -> unit) -> tag -> unit
|
|
35 |
val write_close: (string -> unit) -> tag -> unit
|
|
36 |
|
|
37 |
val html: { lang : string } -> tag list -> tag
|
|
38 |
val head: { title : string, stylesheet_href : string } -> tag list -> tag
|
|
39 |
val body: common_atts -> tag list -> tag
|
|
40 |
val divele: common_atts -> tag list -> tag
|
|
41 |
val span: common_atts * string -> tag
|
|
42 |
val span': common_atts -> tag list -> tag
|
|
43 |
|
|
44 |
val pre: common_atts -> string -> tag
|
|
45 |
|
|
46 |
val table: common_atts -> tag list -> tag
|
|
47 |
val thead: common_atts -> tag list -> tag
|
|
48 |
val tbody: common_atts -> tag list -> tag
|
|
49 |
val tr: tag list -> tag
|
|
50 |
val th: common_atts * string -> tag
|
|
51 |
val th': common_atts -> tag list -> tag
|
|
52 |
val td: common_atts * string -> tag
|
|
53 |
val td': common_atts -> tag list -> tag
|
|
54 |
val td'': common_atts * { colspan : int option, rowspan : int option }
|
|
55 |
-> tag list -> tag
|
|
56 |
|
|
57 |
val p: common_atts * string -> tag
|
|
58 |
val p': common_atts * tag list -> tag
|
|
59 |
val h: common_atts * int * string -> tag
|
|
60 |
val strong: string -> tag
|
|
61 |
val em: string -> tag
|
|
62 |
val a: { href : string, text : string } -> tag
|
|
63 |
|
|
64 |
val ul: common_atts * tag list -> tag
|
|
65 |
val ol: common_atts * tag list -> tag
|
|
66 |
val dl: common_atts * (string * tag) list -> tag
|
|
67 |
|
|
68 |
val alternate_class: { class0 : string, class1 : string }
|
|
69 |
-> tag list -> tag list
|
|
70 |
|
|
71 |
val form: common_atts * { method : string, action : string }
|
|
72 |
-> tag list -> tag
|
|
73 |
|
|
74 |
datatype input_type =
|
|
75 |
TextInput of { value: string option, maxlength: int option }
|
|
76 |
| Password of int option
|
|
77 |
| Checkbox of { checked : bool, value : string option }
|
|
78 |
| Radio of { checked : bool, value : string option }
|
|
79 |
| Submit
|
|
80 |
| Reset
|
|
81 |
| Hidden
|
|
82 |
| Image of { src : string, alt : string }
|
|
83 |
| File of { accept : string }
|
|
84 |
| Button;
|
|
85 |
|
|
86 |
val input: common_atts * { name : string, itype : input_type } -> tag
|
|
87 |
val select: common_atts * { name : string, value : string option }
|
|
88 |
-> string list -> tag
|
|
89 |
val label: common_atts * { for: string } * string -> tag
|
|
90 |
|
|
91 |
val reset_button: common_atts -> tag
|
|
92 |
val submit_button: common_atts -> tag
|
|
93 |
|
|
94 |
datatype event =
|
|
95 |
(* global *)
|
|
96 |
OnClick
|
|
97 |
| OnDblClick
|
|
98 |
| OnMouseDown
|
|
99 |
| OnMouseUp
|
|
100 |
| OnMouseOver
|
|
101 |
| OnMouseMove
|
|
102 |
| OnMouseOut
|
|
103 |
| OnKeyPress
|
|
104 |
| OnKeyDown
|
|
105 |
| OnKeyUp
|
|
106 |
(* anchor/label/input/select/textarea/button/area *)
|
|
107 |
| OnFocus
|
|
108 |
| OnBlur
|
|
109 |
(* form *)
|
|
110 |
| OnSubmit
|
|
111 |
| OnReset
|
|
112 |
(* input/textarea *)
|
|
113 |
| OnSelect
|
|
114 |
(* input/select/textarea *)
|
|
115 |
| OnChange
|
|
116 |
(* body *)
|
|
117 |
| OnLoad
|
|
118 |
| OnUnload;
|
|
119 |
|
|
120 |
val script: common_atts * { script_type: string, src: string } -> tag
|
|
121 |
val add_script: event * string -> tag -> tag
|
|
122 |
end;
|
|
123 |
|
|
124 |
structure Xhtml : XHTML =
|
|
125 |
struct
|
|
126 |
|
|
127 |
type attribute = string * string;
|
|
128 |
type common_atts = {
|
|
129 |
id : string option,
|
|
130 |
class : string option
|
|
131 |
};
|
|
132 |
val noid = { id = NONE, class = NONE };
|
|
133 |
fun id s = { id = SOME s, class = NONE };
|
|
134 |
fun class s = { id = NONE, class = SOME s };
|
|
135 |
|
|
136 |
fun from_common { id = NONE, class = NONE } = []
|
|
137 |
| from_common { id = SOME i, class = NONE } = [("id", i)]
|
|
138 |
| from_common { id = NONE, class = SOME c } = [("class", c)]
|
|
139 |
| from_common { id = SOME i, class = SOME c } = [("id", i), ("class", c)];
|
|
140 |
|
|
141 |
val update_atts =
|
|
142 |
AList.join (op = : string * string -> bool) (fn _ => snd);
|
|
143 |
|
|
144 |
datatype tag = Tag of (string * attribute list * tag list)
|
|
145 |
| Text of string
|
|
146 |
| RawText of string;
|
|
147 |
|
|
148 |
fun is_text (Tag _) = false
|
|
149 |
| is_text (Text _) = true
|
|
150 |
| is_text (RawText _) = true;
|
|
151 |
|
|
152 |
fun is_tag (Tag _) = true
|
|
153 |
| is_tag (Text _) = false
|
|
154 |
| is_tag (RawText _) = false;
|
|
155 |
|
|
156 |
val att = pair;
|
|
157 |
|
|
158 |
fun bool_att (nm, true) = [(nm, nm)]
|
|
159 |
| bool_att (nm, false) = [];
|
|
160 |
|
|
161 |
fun tag name atts inner = Tag (name, atts, inner);
|
|
162 |
fun tag' name common_atts inner = Tag (name, from_common common_atts, inner);
|
|
163 |
fun text t = Text t;
|
|
164 |
fun raw_text t = RawText t;
|
|
165 |
|
|
166 |
fun add_attributes atts' (Tag (nm, atts, inner)) =
|
|
167 |
Tag (nm, update_atts (atts, atts'), inner)
|
|
168 |
| add_attributes _ t = t;
|
|
169 |
|
|
170 |
fun append (Tag (nm, atts, inner)) inner' = Tag (nm, atts, inner @ inner')
|
|
171 |
| append _ _ = raise Fail "cannot append to a text element";
|
|
172 |
|
|
173 |
fun show_att (n, v) = concat [" ", n, "=\"", XML.text v, "\""];
|
|
174 |
|
|
175 |
fun show_text (Text t) = XML.text t
|
|
176 |
| show_text (RawText t) = t
|
|
177 |
| show_text _ = raise Fail "Bad call to show_text.";
|
|
178 |
|
|
179 |
fun show (Text t) = [XML.text t]
|
|
180 |
| show (RawText t) = [t]
|
|
181 |
| show (Tag (nm, atts, inner)) =
|
|
182 |
(["<", nm] @ map show_att atts
|
|
183 |
@
|
|
184 |
(if length inner = 0
|
|
185 |
then ["/>"]
|
41455
|
186 |
else flat (
|
33817
|
187 |
[[">"]]
|
|
188 |
@
|
|
189 |
map show inner
|
|
190 |
@
|
|
191 |
[["</", nm, ">"]]
|
|
192 |
)));
|
|
193 |
|
|
194 |
fun write pr =
|
|
195 |
let
|
|
196 |
fun f (Text t) = (pr o XML.text) t
|
|
197 |
| f (RawText t) = pr t
|
|
198 |
| f (Tag (nm, atts, inner)) = (
|
|
199 |
pr "<";
|
|
200 |
pr nm;
|
|
201 |
app (pr o show_att) atts;
|
|
202 |
if length inner = 0
|
|
203 |
then pr "/>"
|
|
204 |
else (
|
|
205 |
pr ">";
|
|
206 |
app f inner;
|
|
207 |
pr ("</" ^ nm ^ ">")
|
|
208 |
))
|
|
209 |
in f end;
|
|
210 |
|
|
211 |
(* Print all opening tags down into the tree until a branch of degree > 1 is
|
|
212 |
found, in which case print everything before the last tag, which is then
|
|
213 |
opened. *)
|
|
214 |
fun write_open pr =
|
|
215 |
let
|
|
216 |
fun f (Text t) = (pr o XML.text) t
|
|
217 |
| f (RawText t) = pr t
|
|
218 |
| f (Tag (nm, atts, [])) =
|
|
219 |
(pr "<"; pr nm; app (pr o show_att) atts; pr ">")
|
|
220 |
| f (Tag (nm, atts, xs)) =
|
|
221 |
(pr "<"; pr nm; app (pr o show_att) atts; pr ">";
|
|
222 |
(case take_suffix is_text xs of
|
|
223 |
([], _) => ()
|
|
224 |
| (b, _) =>
|
|
225 |
let val (xs, x) = split_last b;
|
|
226 |
in app (write pr) xs; f x end));
|
|
227 |
in f end;
|
|
228 |
|
|
229 |
(* Print matching closing tags for write_open. *)
|
|
230 |
fun write_close pr =
|
|
231 |
let
|
|
232 |
fun close nm = pr ("</" ^ nm ^ ">");
|
|
233 |
val pr_text = app (pr o show_text);
|
|
234 |
|
|
235 |
fun f (Text t) = ()
|
|
236 |
| f (RawText t) = ()
|
|
237 |
| f (Tag (nm, _, [])) = close nm
|
|
238 |
| f (Tag (nm, _, xs)) =
|
|
239 |
(case take_suffix is_text xs of
|
|
240 |
([], text) => pr_text text
|
|
241 |
| (b, text) =>
|
|
242 |
let val (xs, x) = split_last b;
|
|
243 |
in f x; close nm; pr_text text end);
|
|
244 |
in f end;
|
|
245 |
|
|
246 |
fun html { lang } tags = Tag ("html",
|
|
247 |
[("xmlns", "http://www.w3.org/1999/xhtml"),
|
|
248 |
("xml:lang", lang)],
|
|
249 |
tags);
|
|
250 |
|
|
251 |
fun head { title, stylesheet_href } inner = let
|
|
252 |
val link =
|
|
253 |
Tag ("link",
|
|
254 |
[("rel", "stylesheet"),
|
|
255 |
("type", "text/css"),
|
|
256 |
("href", stylesheet_href)], []);
|
|
257 |
val title = Tag ("title", [], [Text title]);
|
|
258 |
val charset = Tag ("meta",
|
|
259 |
[("http-equiv", "Content-type"),
|
|
260 |
("content", "text/html; charset=UTF-8")], []);
|
|
261 |
in Tag ("head", [], link::title::charset::inner) end;
|
|
262 |
|
|
263 |
fun body common_atts tags = Tag ("body", from_common common_atts, tags);
|
|
264 |
|
|
265 |
fun divele common_atts tags = Tag ("div", from_common common_atts, tags);
|
|
266 |
fun span (common_atts, t) = Tag ("span", from_common common_atts, [Text t]);
|
|
267 |
fun span' common_atts tags = Tag ("span", from_common common_atts, tags);
|
|
268 |
|
|
269 |
fun pre common_atts rt = Tag ("pre", from_common common_atts, [RawText rt]);
|
|
270 |
|
|
271 |
fun ostr_att (nm, NONE) = []
|
|
272 |
| ostr_att (nm, SOME s) = [(nm, s)];
|
41491
|
273 |
val oint_att = ostr_att o apsnd (Option.map string_of_int);
|
33817
|
274 |
|
|
275 |
val table = tag' "table";
|
|
276 |
val thead = tag' "thead";
|
|
277 |
val tbody = tag' "tbody";
|
|
278 |
val tr = tag "tr" [];
|
|
279 |
fun th (common_atts, t) = Tag ("th", from_common common_atts, [Text t]);
|
|
280 |
fun th' common_atts tags = Tag ("th", from_common common_atts, tags);
|
|
281 |
fun td (common_atts, t) = Tag ("td", from_common common_atts, [Text t]);
|
|
282 |
fun td' common_atts tags = Tag ("td", from_common common_atts, tags);
|
|
283 |
fun td'' (common_atts, { colspan, rowspan }) tags =
|
|
284 |
Tag ("td",
|
|
285 |
from_common common_atts
|
|
286 |
@ oint_att ("colspan", colspan)
|
|
287 |
@ oint_att ("rowspan", rowspan),
|
|
288 |
tags);
|
|
289 |
|
|
290 |
fun p (common_atts, t) = Tag ("p", from_common common_atts, [Text t]);
|
|
291 |
fun p' (common_atts, tags) = Tag ("p", from_common common_atts, tags);
|
|
292 |
|
|
293 |
fun h (common_atts, i, text) =
|
41491
|
294 |
Tag ("h" ^ string_of_int i, from_common common_atts, [Text text]);
|
33817
|
295 |
|
|
296 |
fun strong t = Tag ("strong", [], [Text t]);
|
|
297 |
fun em t = Tag ("em", [], [Text t]);
|
|
298 |
fun a { href, text } = Tag ("a", [("href", href)], [Text text]);
|
|
299 |
|
|
300 |
fun to_li tag = Tag ("li", [], [tag]);
|
|
301 |
fun ul (common_atts, lis) = Tag ("ul", from_common common_atts, map to_li lis);
|
|
302 |
fun ol (common_atts, lis) = Tag ("ol", from_common common_atts, map to_li lis);
|
|
303 |
|
|
304 |
fun to_dtdd (nm, tag) = [Tag ("dt", [], [Text nm]),
|
|
305 |
Tag ("dd", [], [tag])];
|
|
306 |
fun dl (common_atts, dtdds) =
|
41455
|
307 |
Tag ("dl", from_common common_atts, maps to_dtdd dtdds);
|
33817
|
308 |
|
|
309 |
fun alternate_class { class0, class1 } rows = let
|
|
310 |
fun f ((true, xs), x) = (false, add_attributes [("class", class0)] x :: xs)
|
|
311 |
| f ((false, xs), x) = (true, add_attributes [("class", class1)] x :: xs);
|
|
312 |
in Library.foldl f ((true, []), rows) |> snd |> rev end;
|
|
313 |
|
|
314 |
fun form (common_atts as { id, ... }, { method, action }) tags =
|
|
315 |
Tag ("form",
|
|
316 |
[("method", method),
|
|
317 |
("action", action)]
|
|
318 |
@ from_common common_atts, tags);
|
|
319 |
|
|
320 |
datatype input_type =
|
|
321 |
TextInput of { value: string option, maxlength: int option }
|
|
322 |
| Password of int option
|
|
323 |
| Checkbox of { checked : bool, value : string option }
|
|
324 |
| Radio of { checked : bool, value : string option }
|
|
325 |
| Submit
|
|
326 |
| Reset
|
|
327 |
| Hidden
|
|
328 |
| Image of { src : string, alt : string }
|
|
329 |
| File of { accept : string }
|
|
330 |
| Button;
|
|
331 |
|
|
332 |
fun from_checked { checked = false, value = NONE } = []
|
|
333 |
| from_checked { checked = true, value = NONE } = [("checked", "checked")]
|
|
334 |
| from_checked { checked = false, value = SOME v } = [("value", v)]
|
|
335 |
| from_checked { checked = true, value = SOME v } =
|
|
336 |
[("checked", "checked"), ("value", v)];
|
|
337 |
|
|
338 |
fun input_atts (TextInput { value, maxlength }) =
|
|
339 |
("type", "text")
|
|
340 |
:: ostr_att ("value", value)
|
|
341 |
@ oint_att ("maxlength", maxlength)
|
|
342 |
| input_atts (Password NONE) = [("type", "password")]
|
|
343 |
| input_atts (Password (SOME i)) =
|
41491
|
344 |
[("type", "password"), ("maxlength", string_of_int i)]
|
33817
|
345 |
| input_atts (Checkbox checked) =
|
|
346 |
("type", "checkbox") :: from_checked checked
|
|
347 |
| input_atts (Radio checked) = ("type", "radio") :: from_checked checked
|
|
348 |
| input_atts Submit = [("type", "submit")]
|
|
349 |
| input_atts Reset = [("type", "reset")]
|
|
350 |
| input_atts Hidden = [("type", "hidden")]
|
|
351 |
| input_atts (Image { src, alt }) =
|
|
352 |
[("type", "image"), ("src", src), ("alt", alt)]
|
|
353 |
| input_atts (File { accept }) = [("type", "file"), ("accept", accept)]
|
|
354 |
| input_atts Button = [("type", "button")];
|
|
355 |
|
|
356 |
fun input (common_atts, { name, itype }) =
|
|
357 |
Tag ("input",
|
|
358 |
input_atts itype @ [("name", name)] @ from_common common_atts,
|
|
359 |
[]);
|
|
360 |
|
|
361 |
fun reset_button common_atts =
|
|
362 |
Tag ("input", input_atts Reset @ from_common common_atts, []);
|
|
363 |
|
|
364 |
fun submit_button common_atts =
|
|
365 |
Tag ("input", input_atts Submit @ from_common common_atts, []);
|
|
366 |
|
|
367 |
|
|
368 |
fun select (common_atts, { name, value }) options =
|
|
369 |
let
|
|
370 |
fun is_selected t =
|
|
371 |
(case value of
|
|
372 |
NONE => []
|
|
373 |
| SOME s => if t = s then bool_att ("selected", true) else []);
|
|
374 |
fun to_option t = Tag ("option", is_selected t, [Text t]);
|
|
375 |
in
|
|
376 |
Tag ("select",
|
|
377 |
("name", name) :: from_common common_atts,
|
|
378 |
map to_option options)
|
|
379 |
end;
|
|
380 |
|
|
381 |
fun label (common_atts, { for }, text) =
|
|
382 |
Tag ("label", ("for", for) :: from_common common_atts, [Text text]);
|
|
383 |
|
|
384 |
datatype event =
|
|
385 |
OnClick
|
|
386 |
| OnDblClick
|
|
387 |
| OnMouseDown
|
|
388 |
| OnMouseUp
|
|
389 |
| OnMouseOver
|
|
390 |
| OnMouseMove
|
|
391 |
| OnMouseOut
|
|
392 |
| OnKeyPress
|
|
393 |
| OnKeyDown
|
|
394 |
| OnKeyUp
|
|
395 |
| OnFocus
|
|
396 |
| OnBlur
|
|
397 |
| OnSubmit
|
|
398 |
| OnReset
|
|
399 |
| OnSelect
|
|
400 |
| OnChange
|
|
401 |
| OnLoad
|
|
402 |
| OnUnload;
|
|
403 |
|
|
404 |
fun event_to_str OnClick = "onclick"
|
|
405 |
| event_to_str OnDblClick = "ondblclick"
|
|
406 |
| event_to_str OnMouseDown = "onmousedown"
|
|
407 |
| event_to_str OnMouseUp = "onmouseup"
|
|
408 |
| event_to_str OnMouseOver = "onmouseover"
|
|
409 |
| event_to_str OnMouseMove = "onmousemove"
|
|
410 |
| event_to_str OnMouseOut = "onmouseout"
|
|
411 |
| event_to_str OnKeyPress = "onkeypress"
|
|
412 |
| event_to_str OnKeyDown = "onkeydown"
|
|
413 |
| event_to_str OnKeyUp = "onkeyup"
|
|
414 |
| event_to_str OnFocus = "onfocus"
|
|
415 |
| event_to_str OnBlur = "onblur"
|
|
416 |
| event_to_str OnSubmit = "onsubmit"
|
|
417 |
| event_to_str OnReset = "onreset"
|
|
418 |
| event_to_str OnSelect = "onselect"
|
|
419 |
| event_to_str OnChange = "onchange"
|
|
420 |
| event_to_str OnLoad = "onload"
|
|
421 |
| event_to_str OnUnload = "onunload";
|
|
422 |
|
|
423 |
fun script (common_atts, {script_type, src}) =
|
|
424 |
Tag ("script",
|
|
425 |
("type", script_type)
|
|
426 |
:: ("src", src)
|
|
427 |
:: from_common common_atts, [text ""]);
|
|
428 |
|
|
429 |
fun add_script (evty, script) (Tag (name, atts, inner))
|
|
430 |
= Tag (name, AList.update (op =) (event_to_str evty, script) atts, inner)
|
|
431 |
| add_script _ t = t;
|
|
432 |
|
|
433 |
|
|
434 |
val doctype_xhtml1_0_strict =
|
|
435 |
"<!DOCTYPE html PUBLIC \"-//W3C//DTD XHTML 1.0 Strict//EN\" \
|
|
436 |
\\"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd\">\n";
|
|
437 |
|
|
438 |
end;
|
|
439 |
|