|
1 (* Title: html_unicode.ML |
|
2 Author: Timothy Bourke, NICTA |
|
3 Based on Pure/Thy/html.ML |
|
4 by Markus Wenzel and Stefan Berghofer, TU Muenchen |
|
5 |
|
6 HTML presentation elements that use unicode code points. |
|
7 *) |
|
8 |
|
9 signature HTML_UNICODE = |
|
10 sig |
|
11 val print_mode: ('a -> 'b) -> 'a -> 'b |
|
12 end; |
|
13 |
|
14 structure HTML_Unicode: HTML_UNICODE = |
|
15 struct |
|
16 |
|
17 (** HTML print modes **) |
|
18 |
|
19 (* mode *) |
|
20 |
|
21 val htmlunicodeN = "HTMLUnicode"; |
|
22 fun print_mode f x = PrintMode.with_modes [htmlunicodeN, Symbol.xsymbolsN] f x; |
|
23 |
|
24 (* symbol output *) |
|
25 |
|
26 local |
|
27 val sym_width_lookup = Symtab.make |
|
28 [("\<spacespace>", 2), |
|
29 ("\<Longleftarrow>", 2), |
|
30 ("\<longleftarrow>", 2), |
|
31 ("\<Longrightarrow>", 2), |
|
32 ("\<longrightarrow>", 2), |
|
33 ("\<longleftrightarrow>", 2), |
|
34 ("\<^bsub>", 0), |
|
35 ("\<^esub>", 0), |
|
36 ("\<^bsup>", 0), |
|
37 ("\<^esup>", 0)]; |
|
38 |
|
39 fun sym_width s = |
|
40 (case Symtab.lookup sym_width_lookup s of |
|
41 NONE => 1 |
|
42 | SOME w => w); |
|
43 |
|
44 fun output_sym s = |
|
45 if Symbol.is_raw s then (1, Symbol.decode_raw s) |
|
46 else |
|
47 (case UnicodeSymbols.symbol_to_unicode s of |
|
48 SOME x => (sym_width s, "&#" ^ Int.toString x ^ ";") (* numeric entities *) |
|
49 (* SOME x => (sym_width s, UnicodeSymbols.utf8 [x]) (* utf-8 *) *) |
|
50 | NONE => (size s, XML.text s)); |
|
51 |
|
52 fun output_sub s = apsnd (enclose "<sub>" "</sub>") (output_sym s); |
|
53 fun output_sup s = apsnd (enclose "<sup>" "</sup>") (output_sym s); |
|
54 fun output_loc s = apsnd (enclose "<span class=\"loc\">" "</span>") (output_sym s); |
|
55 |
|
56 fun output_syms ("\<^sub>" :: s :: ss) = output_sub s :: output_syms ss |
|
57 | output_syms ("\<^isub>" :: s :: ss) = output_sub s :: output_syms ss |
|
58 | output_syms ("\<^sup>" :: s :: ss) = output_sup s :: output_syms ss |
|
59 | output_syms ("\<^isup>" :: s :: ss) = output_sup s :: output_syms ss |
|
60 | output_syms ("\<^loc>" :: s :: ss) = output_loc s :: output_syms ss |
|
61 | output_syms (s :: ss) = output_sym s :: output_syms ss |
|
62 | output_syms [] = []; |
|
63 |
|
64 fun output_width str = |
|
65 if not (exists_string (fn s => s = "\\" orelse s = "<" orelse s = ">" orelse s = "&") str) |
|
66 then Output.default_output str |
|
67 else |
|
68 let val (syms, width) = fold_map (fn (w, s) => fn width => (s, w + width)) |
|
69 (output_syms (Symbol.explode str)) 0 |
|
70 in (implode syms, width) end; |
|
71 in |
|
72 |
|
73 val output = #1 o output_width; |
|
74 |
|
75 val _ = Output.add_mode htmlunicodeN output_width Symbol.encode_raw; |
|
76 |
|
77 end; |
|
78 |
|
79 (* common markup *) |
|
80 |
|
81 fun span s = ("<span class=" ^ quote (XML.text s) ^ ">", "</span>"); |
|
82 |
|
83 val _ = Markup.add_mode htmlunicodeN (fn (name, _) => span name); |
|
84 |
|
85 end; |