author | wenzelm |
Mon, 16 Nov 2020 22:23:04 +0100 | |
changeset 72622 | 830222403681 |
parent 69804 | 9efccbad7d42 |
child 72636 | 09ee9eb7a3d3 |
permissions | -rw-r--r-- |
24584 | 1 |
(* Title: Pure/Thy/html.ML |
72622
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
69804
diff
changeset
|
2 |
Author: Makarius |
6324 | 3 |
|
9415 | 4 |
HTML presentation elements. |
6324 | 5 |
*) |
6 |
||
7 |
signature HTML = |
|
8 |
sig |
|
61381 | 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 |
|
23622 | 13 |
type text = string |
72622
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
69804
diff
changeset
|
14 |
val name: symbols -> string -> text |
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
69804
diff
changeset
|
15 |
val keyword: symbols -> string -> text |
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
69804
diff
changeset
|
16 |
val command: symbols -> string -> text |
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
69804
diff
changeset
|
17 |
val href_name: string -> string -> string |
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
69804
diff
changeset
|
18 |
val href_path: Url.T -> string -> string |
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
69804
diff
changeset
|
19 |
val href_opt_path: Url.T option -> string -> string |
61381 | 20 |
val begin_document: symbols -> string -> text |
23724 | 21 |
val end_document: text |
6324 | 22 |
end; |
23 |
||
24 |
structure HTML: HTML = |
|
25 |
struct |
|
26 |
||
27 |
||
33985 | 28 |
(* common markup *) |
29 |
||
67306 | 30 |
fun span "" = ("<span>", "</span>") |
31 |
| span class = ("<span class=" ^ quote (XML.text class) ^ ">", "</span>"); |
|
32 |
||
66044 | 33 |
val enclose_span = uncurry enclose o span; |
33985 | 34 |
|
66044 | 35 |
val hidden = enclose_span Markup.hiddenN; |
33985 | 36 |
|
37 |
||
6324 | 38 |
(* symbol output *) |
39 |
||
61381 | 40 |
abstype symbols = Symbols of string Symtab.table |
41 |
with |
|
42 |
||
43 |
fun make_symbols codes = |
|
44 |
let |
|
45 |
val mapping = |
|
63806 | 46 |
map (apsnd (fn c => "&#" ^ Value.print_int c ^ ";")) codes @ |
61381 | 47 |
[("'", "'"), |
62529
8b7bdfc09f3b
clarified treatment of fragments of Isabelle symbols during bootstrap;
wenzelm
parents:
61381
diff
changeset
|
48 |
("\<^bsub>", hidden "⇘" ^ "<sub>"), |
8b7bdfc09f3b
clarified treatment of fragments of Isabelle symbols during bootstrap;
wenzelm
parents:
61381
diff
changeset
|
49 |
("\<^esub>", hidden "⇙" ^ "</sub>"), |
8b7bdfc09f3b
clarified treatment of fragments of Isabelle symbols during bootstrap;
wenzelm
parents:
61381
diff
changeset
|
50 |
("\<^bsup>", hidden "⇗" ^ "<sup>"), |
8b7bdfc09f3b
clarified treatment of fragments of Isabelle symbols during bootstrap;
wenzelm
parents:
61381
diff
changeset
|
51 |
("\<^esup>", hidden "⇖" ^ "</sup>")]; |
61381 | 52 |
in Symbols (fold Symtab.update mapping Symtab.empty) end; |
53 |
||
54 |
val no_symbols = make_symbols []; |
|
55 |
||
56 |
fun output_sym (Symbols tab) s = |
|
63934 | 57 |
(case Symtab.lookup tab s of |
58 |
SOME x => x |
|
59 |
| NONE => XML.text s); |
|
61381 | 60 |
|
61 |
end; |
|
62 |
||
6338 | 63 |
local |
61376
93224745477f
output HTML text according to Isabelle/Scala Symbol.Interpretation;
wenzelm
parents:
61374
diff
changeset
|
64 |
|
61381 | 65 |
fun output_markup (bg, en) symbols s1 s2 = |
66 |
hidden s1 ^ enclose bg en (output_sym symbols s2); |
|
61376
93224745477f
output HTML text according to Isabelle/Scala Symbol.Interpretation;
wenzelm
parents:
61374
diff
changeset
|
67 |
|
93224745477f
output HTML text according to Isabelle/Scala Symbol.Interpretation;
wenzelm
parents:
61374
diff
changeset
|
68 |
val output_sub = output_markup ("<sub>", "</sub>"); |
93224745477f
output HTML text according to Isabelle/Scala Symbol.Interpretation;
wenzelm
parents:
61374
diff
changeset
|
69 |
val output_sup = output_markup ("<sup>", "</sup>"); |
93224745477f
output HTML text according to Isabelle/Scala Symbol.Interpretation;
wenzelm
parents:
61374
diff
changeset
|
70 |
val output_bold = output_markup (span "bold"); |
17178 | 71 |
|
61381 | 72 |
fun output_syms _ [] result = implode (rev result) |
73 |
| output_syms symbols (s1 :: rest) result = |
|
61376
93224745477f
output HTML text according to Isabelle/Scala Symbol.Interpretation;
wenzelm
parents:
61374
diff
changeset
|
74 |
let |
93224745477f
output HTML text according to Isabelle/Scala Symbol.Interpretation;
wenzelm
parents:
61374
diff
changeset
|
75 |
val (s2, ss) = (case rest of [] => ("", []) | s2 :: ss => (s2, ss)); |
61381 | 76 |
val (s, r) = |
62529
8b7bdfc09f3b
clarified treatment of fragments of Isabelle symbols during bootstrap;
wenzelm
parents:
61381
diff
changeset
|
77 |
if s1 = "\<^sub>" then (output_sub symbols "⇩" s2, ss) |
8b7bdfc09f3b
clarified treatment of fragments of Isabelle symbols during bootstrap;
wenzelm
parents:
61381
diff
changeset
|
78 |
else if s1 = "\<^sup>" then (output_sup symbols "⇧" s2, ss) |
8b7bdfc09f3b
clarified treatment of fragments of Isabelle symbols during bootstrap;
wenzelm
parents:
61381
diff
changeset
|
79 |
else if s1 = "\<^bold>" then (output_bold symbols "❙" s2, ss) |
61381 | 80 |
else (output_sym symbols s1, rest); |
81 |
in output_syms symbols r (s :: result) end; |
|
14534 | 82 |
|
6338 | 83 |
in |
6324 | 84 |
|
61381 | 85 |
fun output symbols str = output_syms symbols (Symbol.explode str) []; |
61376
93224745477f
output HTML text according to Isabelle/Scala Symbol.Interpretation;
wenzelm
parents:
61374
diff
changeset
|
86 |
|
6338 | 87 |
end; |
88 |
||
6324 | 89 |
|
61379
c57820ceead3
more direct HTML presentation, without print mode;
wenzelm
parents:
61376
diff
changeset
|
90 |
(* presentation *) |
c57820ceead3
more direct HTML presentation, without print mode;
wenzelm
parents:
61376
diff
changeset
|
91 |
|
61381 | 92 |
fun present_span symbols keywords = |
93 |
let |
|
66044 | 94 |
fun present_markup (name, props) = |
95 |
(case Properties.get props Markup.kindN of |
|
96 |
SOME kind => |
|
97 |
if kind = Markup.commandN orelse kind = Markup.keywordN then enclose_span kind else I |
|
98 |
| NONE => I) #> enclose_span name; |
|
61381 | 99 |
fun present_token tok = |
66044 | 100 |
fold_rev present_markup (Token.markups keywords tok) |
101 |
(output symbols (Token.unparse tok)); |
|
61381 | 102 |
in implode o map present_token o Command_Span.content end; |
61379
c57820ceead3
more direct HTML presentation, without print mode;
wenzelm
parents:
61376
diff
changeset
|
103 |
|
c57820ceead3
more direct HTML presentation, without print mode;
wenzelm
parents:
61376
diff
changeset
|
104 |
|
6324 | 105 |
|
106 |
(** HTML markup **) |
|
107 |
||
108 |
type text = string; |
|
109 |
||
110 |
||
111 |
(* atoms *) |
|
112 |
||
61381 | 113 |
val name = enclose "<span class=\"name\">" "</span>" oo output; |
114 |
val keyword = enclose "<span class=\"keyword\">" "</span>" oo output; |
|
115 |
val command = enclose "<span class=\"command\">" "</span>" oo output; |
|
6324 | 116 |
|
117 |
||
118 |
(* misc *) |
|
119 |
||
28840 | 120 |
fun href_name s txt = "<a href=" ^ quote s ^ ">" ^ txt ^ "</a>"; |
21858
05f57309170c
avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents:
20742
diff
changeset
|
121 |
fun href_path path txt = href_name (Url.implode path) txt; |
6376 | 122 |
|
15531 | 123 |
fun href_opt_path NONE txt = txt |
124 |
| href_opt_path (SOME p) txt = href_path p txt; |
|
6376 | 125 |
|
6324 | 126 |
|
127 |
(* document *) |
|
128 |
||
61381 | 129 |
fun begin_document symbols title = |
69804 | 130 |
XML.header ^ |
62529
8b7bdfc09f3b
clarified treatment of fragments of Isabelle symbols during bootstrap;
wenzelm
parents:
61381
diff
changeset
|
131 |
"<!DOCTYPE html PUBLIC \"-//W3C//DTD XHTML 1.0 Transitional//EN\" " ^ |
8b7bdfc09f3b
clarified treatment of fragments of Isabelle symbols during bootstrap;
wenzelm
parents:
61381
diff
changeset
|
132 |
"\"http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd\">\n" ^ |
8b7bdfc09f3b
clarified treatment of fragments of Isabelle symbols during bootstrap;
wenzelm
parents:
61381
diff
changeset
|
133 |
"<html xmlns=\"http://www.w3.org/1999/xhtml\">\n" ^ |
8b7bdfc09f3b
clarified treatment of fragments of Isabelle symbols during bootstrap;
wenzelm
parents:
61381
diff
changeset
|
134 |
"<head>\n" ^ |
8b7bdfc09f3b
clarified treatment of fragments of Isabelle symbols during bootstrap;
wenzelm
parents:
61381
diff
changeset
|
135 |
"<meta http-equiv=\"Content-Type\" content=\"text/html; charset=utf-8\"/>\n" ^ |
8b7bdfc09f3b
clarified treatment of fragments of Isabelle symbols during bootstrap;
wenzelm
parents:
61381
diff
changeset
|
136 |
"<title>" ^ output symbols (title ^ " (" ^ Distribution.version ^ ")") ^ "</title>\n" ^ |
8b7bdfc09f3b
clarified treatment of fragments of Isabelle symbols during bootstrap;
wenzelm
parents:
61381
diff
changeset
|
137 |
"<link media=\"all\" rel=\"stylesheet\" type=\"text/css\" href=\"isabelle.css\"/>\n" ^ |
8b7bdfc09f3b
clarified treatment of fragments of Isabelle symbols during bootstrap;
wenzelm
parents:
61381
diff
changeset
|
138 |
"</head>\n" ^ |
8b7bdfc09f3b
clarified treatment of fragments of Isabelle symbols during bootstrap;
wenzelm
parents:
61381
diff
changeset
|
139 |
"\n" ^ |
8b7bdfc09f3b
clarified treatment of fragments of Isabelle symbols during bootstrap;
wenzelm
parents:
61381
diff
changeset
|
140 |
"<body>\n" ^ |
8b7bdfc09f3b
clarified treatment of fragments of Isabelle symbols during bootstrap;
wenzelm
parents:
61381
diff
changeset
|
141 |
"<div class=\"head\">" ^ |
8b7bdfc09f3b
clarified treatment of fragments of Isabelle symbols during bootstrap;
wenzelm
parents:
61381
diff
changeset
|
142 |
"<h1>" ^ output symbols title ^ "</h1>\n"; |
6324 | 143 |
|
14541 | 144 |
val end_document = "\n</div>\n</body>\n</html>\n"; |
6324 | 145 |
|
146 |
end; |