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