author | blanchet |
Tue, 07 Dec 2010 11:56:01 +0100 | |
changeset 41051 | 2ed1b971fc20 |
parent 37744 | 3daaf23b9ab4 |
child 41491 | a2ad5b824051 |
permissions | -rw-r--r-- |
37744 | 1 |
(* Title: Tools/WWW_Find/html_unicode.ML |
33817 | 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"; |
|
37146
f652333bbf8e
renamed structure PrintMode to Print_Mode, keeping the old name as legacy alias for some time;
wenzelm
parents:
33817
diff
changeset
|
22 |
fun print_mode f x = Print_Mode.with_modes [htmlunicodeN, Symbol.xsymbolsN] f x; |
33817 | 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; |