author | wenzelm |
Thu, 10 Oct 2013 12:02:12 +0200 | |
changeset 54320 | b8bd31c7058c |
parent 53021 | d0fa3f446b9d |
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 |
|
50233
eef21a0726f1
removed remains of Oheimb's double-space (cf. 0a5af667dc75);
wenzelm
parents:
43458
diff
changeset
|
28 |
[("\<Longleftarrow>", 2), |
33817 | 29 |
("\<longleftarrow>", 2), |
30 |
("\<Longrightarrow>", 2), |
|
31 |
("\<longrightarrow>", 2), |
|
32 |
("\<longleftrightarrow>", 2), |
|
33 |
("\<^bsub>", 0), |
|
34 |
("\<^esub>", 0), |
|
35 |
("\<^bsup>", 0), |
|
36 |
("\<^esup>", 0)]; |
|
37 |
||
38 |
fun sym_width s = |
|
39 |
(case Symtab.lookup sym_width_lookup s of |
|
40 |
NONE => 1 |
|
41 |
| SOME w => w); |
|
42 |
||
43 |
fun output_sym s = |
|
44 |
if Symbol.is_raw s then (1, Symbol.decode_raw s) |
|
45 |
else |
|
46 |
(case UnicodeSymbols.symbol_to_unicode s of |
|
41491 | 47 |
SOME x => (sym_width s, "&#" ^ string_of_int x ^ ";") (* numeric entities *) |
33817 | 48 |
(* SOME x => (sym_width s, UnicodeSymbols.utf8 [x]) (* utf-8 *) *) |
49 |
| NONE => (size s, XML.text s)); |
|
50 |
||
51 |
fun output_sub s = apsnd (enclose "<sub>" "</sub>") (output_sym s); |
|
52 |
fun output_sup s = apsnd (enclose "<sup>" "</sup>") (output_sym s); |
|
53 |
||
54 |
fun output_syms ("\<^sub>" :: s :: ss) = output_sub s :: output_syms ss |
|
55 |
| output_syms ("\<^sup>" :: s :: ss) = output_sup s :: output_syms ss |
|
56 |
| output_syms (s :: ss) = output_sym s :: output_syms ss |
|
57 |
| output_syms [] = []; |
|
58 |
||
59 |
fun output_width str = |
|
60 |
if not (exists_string (fn s => s = "\\" orelse s = "<" orelse s = ">" orelse s = "&") str) |
|
61 |
then Output.default_output str |
|
62 |
else |
|
63 |
let val (syms, width) = fold_map (fn (w, s) => fn width => (s, w + width)) |
|
64 |
(output_syms (Symbol.explode str)) 0 |
|
65 |
in (implode syms, width) end; |
|
66 |
in |
|
67 |
||
68 |
val output = #1 o output_width; |
|
69 |
||
70 |
val _ = Output.add_mode htmlunicodeN output_width Symbol.encode_raw; |
|
71 |
||
72 |
end; |
|
73 |
||
74 |
(* common markup *) |
|
75 |
||
76 |
fun span s = ("<span class=" ^ quote (XML.text s) ^ ">", "</span>"); |
|
77 |
||
78 |
val _ = Markup.add_mode htmlunicodeN (fn (name, _) => span name); |
|
79 |
||
80 |
end; |