1 (* Title: Pure/Thy/html.ML |
|
2 Author: Makarius |
|
3 |
|
4 HTML presentation elements. |
|
5 *) |
|
6 |
|
7 signature HTML = |
|
8 sig |
|
9 type symbols |
|
10 val make_symbols: (string * int) list -> symbols |
|
11 val no_symbols: symbols |
|
12 val present_span: symbols -> Keyword.keywords -> Command_Span.span -> Output.output |
|
13 type text = string |
|
14 val name: symbols -> string -> text |
|
15 val keyword: symbols -> string -> text |
|
16 val command: symbols -> string -> text |
|
17 val href_name: string -> string -> string |
|
18 val href_path: Url.T -> string -> string |
|
19 val begin_document: symbols -> string -> text |
|
20 val end_document: text |
|
21 end; |
|
22 |
|
23 structure HTML: HTML = |
|
24 struct |
|
25 |
|
26 |
|
27 (* common markup *) |
|
28 |
|
29 fun span "" = ("<span>", "</span>") |
|
30 | span class = ("<span class=" ^ quote (XML.text class) ^ ">", "</span>"); |
|
31 |
|
32 val enclose_span = uncurry enclose o span; |
|
33 |
|
34 val hidden = enclose_span Markup.hiddenN; |
|
35 |
|
36 |
|
37 (* symbol output *) |
|
38 |
|
39 abstype symbols = Symbols of string Symtab.table |
|
40 with |
|
41 |
|
42 fun make_symbols codes = |
|
43 let |
|
44 val mapping = |
|
45 map (apsnd (fn c => "&#" ^ Value.print_int c ^ ";")) codes @ |
|
46 [("'", "'"), |
|
47 ("\<^bsub>", hidden "⇘" ^ "<sub>"), |
|
48 ("\<^esub>", hidden "⇙" ^ "</sub>"), |
|
49 ("\<^bsup>", hidden "⇗" ^ "<sup>"), |
|
50 ("\<^esup>", hidden "⇖" ^ "</sup>")]; |
|
51 in Symbols (fold Symtab.update mapping Symtab.empty) end; |
|
52 |
|
53 val no_symbols = make_symbols []; |
|
54 |
|
55 fun output_sym (Symbols tab) s = |
|
56 (case Symtab.lookup tab s of |
|
57 SOME x => x |
|
58 | NONE => XML.text s); |
|
59 |
|
60 end; |
|
61 |
|
62 local |
|
63 |
|
64 fun output_markup (bg, en) symbols s1 s2 = |
|
65 hidden s1 ^ enclose bg en (output_sym symbols s2); |
|
66 |
|
67 val output_sub = output_markup ("<sub>", "</sub>"); |
|
68 val output_sup = output_markup ("<sup>", "</sup>"); |
|
69 val output_bold = output_markup (span "bold"); |
|
70 |
|
71 fun output_syms _ [] result = implode (rev result) |
|
72 | output_syms symbols (s1 :: rest) result = |
|
73 let |
|
74 val (s2, ss) = (case rest of [] => ("", []) | s2 :: ss => (s2, ss)); |
|
75 val (s, r) = |
|
76 if s1 = "\<^sub>" then (output_sub symbols "⇩" s2, ss) |
|
77 else if s1 = "\<^sup>" then (output_sup symbols "⇧" s2, ss) |
|
78 else if s1 = "\<^bold>" then (output_bold symbols "❙" s2, ss) |
|
79 else (output_sym symbols s1, rest); |
|
80 in output_syms symbols r (s :: result) end; |
|
81 |
|
82 in |
|
83 |
|
84 fun output symbols str = output_syms symbols (Symbol.explode str) []; |
|
85 |
|
86 end; |
|
87 |
|
88 |
|
89 (* presentation *) |
|
90 |
|
91 fun present_span symbols keywords = |
|
92 let |
|
93 fun present_markup (name, props) = |
|
94 (case Properties.get props Markup.kindN of |
|
95 SOME kind => |
|
96 if kind = Markup.commandN orelse kind = Markup.keywordN then enclose_span kind else I |
|
97 | NONE => I) #> enclose_span name; |
|
98 fun present_token tok = |
|
99 fold_rev present_markup (Token.markups keywords tok) |
|
100 (output symbols (Token.unparse tok)); |
|
101 in implode o map present_token o Command_Span.content end; |
|
102 |
|
103 |
|
104 |
|
105 (** HTML markup **) |
|
106 |
|
107 type text = string; |
|
108 |
|
109 |
|
110 (* atoms *) |
|
111 |
|
112 val name = enclose "<span class=\"name\">" "</span>" oo output; |
|
113 val keyword = enclose "<span class=\"keyword\">" "</span>" oo output; |
|
114 val command = enclose "<span class=\"command\">" "</span>" oo output; |
|
115 |
|
116 |
|
117 (* misc *) |
|
118 |
|
119 fun href_name s txt = "<a href=" ^ quote s ^ ">" ^ txt ^ "</a>"; |
|
120 fun href_path path txt = href_name (Url.implode path) txt; |
|
121 |
|
122 |
|
123 (* document *) |
|
124 |
|
125 fun begin_document symbols title = |
|
126 XML.header ^ |
|
127 "<!DOCTYPE html PUBLIC \"-//W3C//DTD XHTML 1.0 Transitional//EN\" " ^ |
|
128 "\"http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd\">\n" ^ |
|
129 "<html xmlns=\"http://www.w3.org/1999/xhtml\">\n" ^ |
|
130 "<head>\n" ^ |
|
131 "<meta http-equiv=\"Content-Type\" content=\"text/html; charset=utf-8\"/>\n" ^ |
|
132 "<title>" ^ output symbols (title ^ " (" ^ Distribution.version ^ ")") ^ "</title>\n" ^ |
|
133 "<link media=\"all\" rel=\"stylesheet\" type=\"text/css\" href=\"isabelle.css\"/>\n" ^ |
|
134 "</head>\n" ^ |
|
135 "\n" ^ |
|
136 "<body>\n" ^ |
|
137 "<div class=\"head\">" ^ |
|
138 "<h1>" ^ output symbols title ^ "</h1>\n"; |
|
139 |
|
140 val end_document = "\n</div>\n</body>\n</html>\n"; |
|
141 |
|
142 end; |
|