author | wenzelm |
Tue, 17 Nov 2020 16:54:49 +0100 | |
changeset 72636 | 09ee9eb7a3d3 |
parent 72622 | 830222403681 |
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 |
61381 | 19 |
val begin_document: symbols -> string -> text |
23724 | 20 |
val end_document: text |
6324 | 21 |
end; |
22 |
||
23 |
structure HTML: HTML = |
|
24 |
struct |
|
25 |
||
26 |
||
33985 | 27 |
(* common markup *) |
28 |
||
67306 | 29 |
fun span "" = ("<span>", "</span>") |
30 |
| span class = ("<span class=" ^ quote (XML.text class) ^ ">", "</span>"); |
|
31 |
||
66044 | 32 |
val enclose_span = uncurry enclose o span; |
33985 | 33 |
|
66044 | 34 |
val hidden = enclose_span Markup.hiddenN; |
33985 | 35 |
|
36 |
||
6324 | 37 |
(* symbol output *) |
38 |
||
61381 | 39 |
abstype symbols = Symbols of string Symtab.table |
40 |
with |
|
41 |
||
42 |
fun make_symbols codes = |
|
43 |
let |
|
44 |
val mapping = |
|
63806 | 45 |
map (apsnd (fn c => "&#" ^ Value.print_int c ^ ";")) codes @ |
61381 | 46 |
[("'", "'"), |
62529
8b7bdfc09f3b
clarified treatment of fragments of Isabelle symbols during bootstrap;
wenzelm
parents:
61381
diff
changeset
|
47 |
("\<^bsub>", hidden "⇘" ^ "<sub>"), |
8b7bdfc09f3b
clarified treatment of fragments of Isabelle symbols during bootstrap;
wenzelm
parents:
61381
diff
changeset
|
48 |
("\<^esub>", hidden "⇙" ^ "</sub>"), |
8b7bdfc09f3b
clarified treatment of fragments of Isabelle symbols during bootstrap;
wenzelm
parents:
61381
diff
changeset
|
49 |
("\<^bsup>", hidden "⇗" ^ "<sup>"), |
8b7bdfc09f3b
clarified treatment of fragments of Isabelle symbols during bootstrap;
wenzelm
parents:
61381
diff
changeset
|
50 |
("\<^esup>", hidden "⇖" ^ "</sup>")]; |
61381 | 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 = |
|
63934 | 56 |
(case Symtab.lookup tab s of |
57 |
SOME x => x |
|
58 |
| NONE => XML.text s); |
|
61381 | 59 |
|
60 |
end; |
|
61 |
||
6338 | 62 |
local |
61376
93224745477f
output HTML text according to Isabelle/Scala Symbol.Interpretation;
wenzelm
parents:
61374
diff
changeset
|
63 |
|
61381 | 64 |
fun output_markup (bg, en) symbols s1 s2 = |
65 |
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
|
66 |
|
93224745477f
output HTML text according to Isabelle/Scala Symbol.Interpretation;
wenzelm
parents:
61374
diff
changeset
|
67 |
val output_sub = output_markup ("<sub>", "</sub>"); |
93224745477f
output HTML text according to Isabelle/Scala Symbol.Interpretation;
wenzelm
parents:
61374
diff
changeset
|
68 |
val output_sup = output_markup ("<sup>", "</sup>"); |
93224745477f
output HTML text according to Isabelle/Scala Symbol.Interpretation;
wenzelm
parents:
61374
diff
changeset
|
69 |
val output_bold = output_markup (span "bold"); |
17178 | 70 |
|
61381 | 71 |
fun output_syms _ [] result = implode (rev result) |
72 |
| output_syms symbols (s1 :: rest) result = |
|
61376
93224745477f
output HTML text according to Isabelle/Scala Symbol.Interpretation;
wenzelm
parents:
61374
diff
changeset
|
73 |
let |
93224745477f
output HTML text according to Isabelle/Scala Symbol.Interpretation;
wenzelm
parents:
61374
diff
changeset
|
74 |
val (s2, ss) = (case rest of [] => ("", []) | s2 :: ss => (s2, ss)); |
61381 | 75 |
val (s, r) = |
62529
8b7bdfc09f3b
clarified treatment of fragments of Isabelle symbols during bootstrap;
wenzelm
parents:
61381
diff
changeset
|
76 |
if s1 = "\<^sub>" then (output_sub symbols "⇩" s2, ss) |
8b7bdfc09f3b
clarified treatment of fragments of Isabelle symbols during bootstrap;
wenzelm
parents:
61381
diff
changeset
|
77 |
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
|
78 |
else if s1 = "\<^bold>" then (output_bold symbols "❙" s2, ss) |
61381 | 79 |
else (output_sym symbols s1, rest); |
80 |
in output_syms symbols r (s :: result) end; |
|
14534 | 81 |
|
6338 | 82 |
in |
6324 | 83 |
|
61381 | 84 |
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
|
85 |
|
6338 | 86 |
end; |
87 |
||
6324 | 88 |
|
61379
c57820ceead3
more direct HTML presentation, without print mode;
wenzelm
parents:
61376
diff
changeset
|
89 |
(* presentation *) |
c57820ceead3
more direct HTML presentation, without print mode;
wenzelm
parents:
61376
diff
changeset
|
90 |
|
61381 | 91 |
fun present_span symbols keywords = |
92 |
let |
|
66044 | 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; |
|
61381 | 98 |
fun present_token tok = |
66044 | 99 |
fold_rev present_markup (Token.markups keywords tok) |
100 |
(output symbols (Token.unparse tok)); |
|
61381 | 101 |
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
|
102 |
|
c57820ceead3
more direct HTML presentation, without print mode;
wenzelm
parents:
61376
diff
changeset
|
103 |
|
6324 | 104 |
|
105 |
(** HTML markup **) |
|
106 |
||
107 |
type text = string; |
|
108 |
||
109 |
||
110 |
(* atoms *) |
|
111 |
||
61381 | 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; |
|
6324 | 115 |
|
116 |
||
117 |
(* misc *) |
|
118 |
||
28840 | 119 |
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
|
120 |
fun href_path path txt = href_name (Url.implode path) txt; |
6376 | 121 |
|
6324 | 122 |
|
123 |
(* document *) |
|
124 |
||
61381 | 125 |
fun begin_document symbols title = |
69804 | 126 |
XML.header ^ |
62529
8b7bdfc09f3b
clarified treatment of fragments of Isabelle symbols during bootstrap;
wenzelm
parents:
61381
diff
changeset
|
127 |
"<!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
|
128 |
"\"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
|
129 |
"<html xmlns=\"http://www.w3.org/1999/xhtml\">\n" ^ |
8b7bdfc09f3b
clarified treatment of fragments of Isabelle symbols during bootstrap;
wenzelm
parents:
61381
diff
changeset
|
130 |
"<head>\n" ^ |
8b7bdfc09f3b
clarified treatment of fragments of Isabelle symbols during bootstrap;
wenzelm
parents:
61381
diff
changeset
|
131 |
"<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
|
132 |
"<title>" ^ output symbols (title ^ " (" ^ Distribution.version ^ ")") ^ "</title>\n" ^ |
8b7bdfc09f3b
clarified treatment of fragments of Isabelle symbols during bootstrap;
wenzelm
parents:
61381
diff
changeset
|
133 |
"<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
|
134 |
"</head>\n" ^ |
8b7bdfc09f3b
clarified treatment of fragments of Isabelle symbols during bootstrap;
wenzelm
parents:
61381
diff
changeset
|
135 |
"\n" ^ |
8b7bdfc09f3b
clarified treatment of fragments of Isabelle symbols during bootstrap;
wenzelm
parents:
61381
diff
changeset
|
136 |
"<body>\n" ^ |
8b7bdfc09f3b
clarified treatment of fragments of Isabelle symbols during bootstrap;
wenzelm
parents:
61381
diff
changeset
|
137 |
"<div class=\"head\">" ^ |
8b7bdfc09f3b
clarified treatment of fragments of Isabelle symbols during bootstrap;
wenzelm
parents:
61381
diff
changeset
|
138 |
"<h1>" ^ output symbols title ^ "</h1>\n"; |
6324 | 139 |
|
14541 | 140 |
val end_document = "\n</div>\n</body>\n</html>\n"; |
6324 | 141 |
|
142 |
end; |