author | wenzelm |
Sun, 21 Aug 2022 11:48:14 +0200 | |
changeset 75939 | 87f0adcb7e10 |
parent 75938 | 17d51bdabded |
child 75940 | c6edbc025fae |
permissions | -rw-r--r-- |
33984 | 1 |
/* Title: Pure/Thy/html.scala |
2 |
Author: Makarius |
|
3 |
||
50707
5b2bf7611662
maintain session index on Scala side, for more determistic results;
wenzelm
parents:
50201
diff
changeset
|
4 |
HTML presentation elements. |
33984 | 5 |
*/ |
6 |
||
7 |
package isabelle |
|
8 |
||
55618 | 9 |
|
75393 | 10 |
object HTML { |
73207 | 11 |
/* attributes */ |
12 |
||
75393 | 13 |
class Attribute(val name: String, value: String) { |
73207 | 14 |
def xml: XML.Attribute = name -> value |
15 |
def apply(elem: XML.Elem): XML.Elem = elem + xml |
|
16 |
} |
|
17 |
||
18 |
def id(s: String): Attribute = new Attribute("id", s) |
|
19 |
def class_(name: String): Attribute = new Attribute("class", name) |
|
20 |
||
21 |
def width(w: Int): Attribute = new Attribute("width", w.toString) |
|
22 |
def height(h: Int): Attribute = new Attribute("height", h.toString) |
|
23 |
def size(w: Int, h: Int)(elem: XML.Elem): XML.Elem = width(w)(height(h)(elem)) |
|
24 |
||
74679 | 25 |
val entity_def: Attribute = class_("entity_def") |
26 |
val entity_ref: Attribute = class_("entity_ref") |
|
27 |
||
73207 | 28 |
|
29 |
/* structured markup operators */ |
|
30 |
||
31 |
def text(txt: String): XML.Body = if (txt.isEmpty) Nil else List(XML.Text(txt)) |
|
32 |
val break: XML.Body = List(XML.elem("br")) |
|
33 |
val nl: XML.Body = List(XML.Text("\n")) |
|
34 |
||
75393 | 35 |
class Operator(val name: String) { |
73207 | 36 |
def apply(body: XML.Body): XML.Elem = XML.elem(name, body) |
37 |
def apply(att: Attribute, body: XML.Body): XML.Elem = att(apply(body)) |
|
38 |
def apply(c: String, body: XML.Body): XML.Elem = apply(class_(c), body) |
|
39 |
} |
|
40 |
||
75393 | 41 |
class Heading(name: String) extends Operator(name) { |
73207 | 42 |
def apply(txt: String): XML.Elem = super.apply(text(txt)) |
43 |
def apply(att: Attribute, txt: String): XML.Elem = super.apply(att, text(txt)) |
|
44 |
def apply(c: String, txt: String): XML.Elem = super.apply(c, text(txt)) |
|
45 |
} |
|
46 |
||
47 |
val div = new Operator("div") |
|
48 |
val span = new Operator("span") |
|
49 |
val pre = new Operator("pre") |
|
50 |
val par = new Operator("p") |
|
51 |
val sub = new Operator("sub") |
|
52 |
val sup = new Operator("sup") |
|
53 |
val emph = new Operator("em") |
|
54 |
val bold = new Operator("b") |
|
55 |
val code = new Operator("code") |
|
56 |
val item = new Operator("li") |
|
57 |
val list = new Operator("ul") |
|
74657
9fcf80ceb863
updated to scala-2.13.7 --- problems with jline disappear after purging $HOME/.inputrc;
wenzelm
parents:
73340
diff
changeset
|
58 |
val `enum` = new Operator("ol") |
73207 | 59 |
val descr = new Operator("dl") |
60 |
val dt = new Operator("dt") |
|
61 |
val dd = new Operator("dd") |
|
62 |
||
63 |
val title = new Heading("title") |
|
64 |
val chapter = new Heading("h1") |
|
65 |
val section = new Heading("h2") |
|
66 |
val subsection = new Heading("h3") |
|
67 |
val subsubsection = new Heading("h4") |
|
68 |
val paragraph = new Heading("h5") |
|
69 |
val subparagraph = new Heading("h6") |
|
70 |
||
71 |
def itemize(items: List[XML.Body]): XML.Elem = list(items.map(item(_))) |
|
74657
9fcf80ceb863
updated to scala-2.13.7 --- problems with jline disappear after purging $HOME/.inputrc;
wenzelm
parents:
73340
diff
changeset
|
72 |
def enumerate(items: List[XML.Body]): XML.Elem = `enum`(items.map(item(_))) |
73207 | 73 |
def description(items: List[(XML.Body, XML.Body)]): XML.Elem = |
74 |
descr(items.flatMap({ case (x, y) => List(dt(x), dd(y)) })) |
|
75 |
||
76 |
def link(href: String, body: XML.Body): XML.Elem = |
|
77 |
XML.Elem(Markup("a", List("href" -> href)), if (body.isEmpty) text(href) else body) |
|
78 |
||
79 |
def link(path: Path, body: XML.Body): XML.Elem = link(path.implode, body) |
|
80 |
||
81 |
def image(src: String, alt: String = ""): XML.Elem = |
|
82 |
XML.Elem(Markup("img", List("src" -> src) ::: proper_string(alt).map("alt" -> _).toList), Nil) |
|
83 |
||
84 |
def source(body: XML.Body): XML.Elem = pre("source", body) |
|
85 |
def source(src: String): XML.Elem = source(text(src)) |
|
86 |
||
87 |
def style(s: String): XML.Elem = XML.elem("style", text(s)) |
|
88 |
def style_file(href: String): XML.Elem = |
|
89 |
XML.Elem(Markup("link", List("rel" -> "stylesheet", "type" -> "text/css", "href" -> href)), Nil) |
|
90 |
def style_file(path: Path): XML.Elem = style_file(Url.print_file(path.file)) |
|
91 |
||
92 |
def script(s: String): XML.Elem = XML.elem("script", text(s)) |
|
93 |
def script_file(href: String): XML.Elem = XML.Elem(Markup("script", List("src" -> href)), Nil) |
|
94 |
def script_file(path: Path): XML.Elem = script_file(Url.print_file(path.file)) |
|
95 |
||
96 |
||
75933 | 97 |
/* href */ |
98 |
||
75938
17d51bdabded
proper fonts_prefix (amending c14409948063): default is "" due to self-cancellation of dir;
wenzelm
parents:
75933
diff
changeset
|
99 |
def relative_href(loc: Path, base: Option[Path] = None): String = { |
75939 | 100 |
val path = |
101 |
base match { |
|
102 |
case None => |
|
103 |
val path = loc.expand |
|
104 |
if (path.is_absolute) Exn.error("Relative href expected: " + path) else path |
|
105 |
case Some(dir) => |
|
106 |
val path1 = dir.absolute_file.toPath |
|
107 |
val path2 = loc.absolute_file.toPath |
|
108 |
try { File.path(path1.relativize(path2).toFile) } |
|
109 |
catch { |
|
110 |
case _: IllegalArgumentException => |
|
111 |
Exn.error("Failed to relativize href " + path2 + " with wrt. base " + path1) |
|
112 |
} |
|
113 |
} |
|
114 |
if (path.is_current) "" else path.implode |
|
75933 | 115 |
} |
116 |
||
117 |
||
65997
e3dc9ea67a62
output control symbols like ML version, with optionally hidden source;
wenzelm
parents:
65993
diff
changeset
|
118 |
/* output text with control symbols */ |
59063 | 119 |
|
73208 | 120 |
private val control: Map[Symbol.Symbol, Operator] = |
65997
e3dc9ea67a62
output control symbols like ML version, with optionally hidden source;
wenzelm
parents:
65993
diff
changeset
|
121 |
Map( |
73206 | 122 |
Symbol.sub -> sub, Symbol.sub_decoded -> sub, |
123 |
Symbol.sup -> sup, Symbol.sup_decoded -> sup, |
|
124 |
Symbol.bold -> bold, Symbol.bold_decoded -> bold) |
|
65997
e3dc9ea67a62
output control symbols like ML version, with optionally hidden source;
wenzelm
parents:
65993
diff
changeset
|
125 |
|
73208 | 126 |
private val control_block_begin: Map[Symbol.Symbol, Operator] = |
62104
fb73c0d7bb37
clarified symbol insertion, depending on buffer encoding;
wenzelm
parents:
60215
diff
changeset
|
127 |
Map( |
73206 | 128 |
Symbol.bsub -> sub, Symbol.bsub_decoded -> sub, |
129 |
Symbol.bsup -> sup, Symbol.bsup_decoded -> sup) |
|
130 |
||
73208 | 131 |
private val control_block_end: Map[Symbol.Symbol, Operator] = |
73206 | 132 |
Map( |
133 |
Symbol.esub -> sub, Symbol.esub_decoded -> sub, |
|
134 |
Symbol.esup -> sup, Symbol.esup_decoded -> sup) |
|
65997
e3dc9ea67a62
output control symbols like ML version, with optionally hidden source;
wenzelm
parents:
65993
diff
changeset
|
135 |
|
e3dc9ea67a62
output control symbols like ML version, with optionally hidden source;
wenzelm
parents:
65993
diff
changeset
|
136 |
def is_control(sym: Symbol.Symbol): Boolean = control.isDefinedAt(sym) |
e3dc9ea67a62
output control symbols like ML version, with optionally hidden source;
wenzelm
parents:
65993
diff
changeset
|
137 |
|
73209
de16d797adbe
more robust HTML output: non-balanced bsub/esub are shown verbatim, e.g. within mixfix declarations (due to extra markup);
wenzelm
parents:
73208
diff
changeset
|
138 |
def is_control_block_begin(sym: Symbol.Symbol): Boolean = control_block_begin.isDefinedAt(sym) |
de16d797adbe
more robust HTML output: non-balanced bsub/esub are shown verbatim, e.g. within mixfix declarations (due to extra markup);
wenzelm
parents:
73208
diff
changeset
|
139 |
def is_control_block_end(sym: Symbol.Symbol): Boolean = control_block_end.isDefinedAt(sym) |
75393 | 140 |
def is_control_block_pair(bg: Symbol.Symbol, en: Symbol.Symbol): Boolean = { |
73209
de16d797adbe
more robust HTML output: non-balanced bsub/esub are shown verbatim, e.g. within mixfix declarations (due to extra markup);
wenzelm
parents:
73208
diff
changeset
|
141 |
val bg_decoded = Symbol.decode(bg) |
de16d797adbe
more robust HTML output: non-balanced bsub/esub are shown verbatim, e.g. within mixfix declarations (due to extra markup);
wenzelm
parents:
73208
diff
changeset
|
142 |
val en_decoded = Symbol.decode(en) |
de16d797adbe
more robust HTML output: non-balanced bsub/esub are shown verbatim, e.g. within mixfix declarations (due to extra markup);
wenzelm
parents:
73208
diff
changeset
|
143 |
bg_decoded == Symbol.bsub_decoded && en_decoded == Symbol.esub_decoded || |
de16d797adbe
more robust HTML output: non-balanced bsub/esub are shown verbatim, e.g. within mixfix declarations (due to extra markup);
wenzelm
parents:
73208
diff
changeset
|
144 |
bg_decoded == Symbol.bsup_decoded && en_decoded == Symbol.esup_decoded |
de16d797adbe
more robust HTML output: non-balanced bsub/esub are shown verbatim, e.g. within mixfix declarations (due to extra markup);
wenzelm
parents:
73208
diff
changeset
|
145 |
} |
de16d797adbe
more robust HTML output: non-balanced bsub/esub are shown verbatim, e.g. within mixfix declarations (due to extra markup);
wenzelm
parents:
73208
diff
changeset
|
146 |
|
75393 | 147 |
def check_control_blocks(body: XML.Body): Boolean = { |
73209
de16d797adbe
more robust HTML output: non-balanced bsub/esub are shown verbatim, e.g. within mixfix declarations (due to extra markup);
wenzelm
parents:
73208
diff
changeset
|
148 |
var ok = true |
de16d797adbe
more robust HTML output: non-balanced bsub/esub are shown verbatim, e.g. within mixfix declarations (due to extra markup);
wenzelm
parents:
73208
diff
changeset
|
149 |
var open = List.empty[Symbol.Symbol] |
de16d797adbe
more robust HTML output: non-balanced bsub/esub are shown verbatim, e.g. within mixfix declarations (due to extra markup);
wenzelm
parents:
73208
diff
changeset
|
150 |
for { XML.Text(text) <- body; sym <- Symbol.iterator(text) } { |
de16d797adbe
more robust HTML output: non-balanced bsub/esub are shown verbatim, e.g. within mixfix declarations (due to extra markup);
wenzelm
parents:
73208
diff
changeset
|
151 |
if (is_control_block_begin(sym)) open ::= sym |
de16d797adbe
more robust HTML output: non-balanced bsub/esub are shown verbatim, e.g. within mixfix declarations (due to extra markup);
wenzelm
parents:
73208
diff
changeset
|
152 |
else if (is_control_block_end(sym)) { |
de16d797adbe
more robust HTML output: non-balanced bsub/esub are shown verbatim, e.g. within mixfix declarations (due to extra markup);
wenzelm
parents:
73208
diff
changeset
|
153 |
open match { |
de16d797adbe
more robust HTML output: non-balanced bsub/esub are shown verbatim, e.g. within mixfix declarations (due to extra markup);
wenzelm
parents:
73208
diff
changeset
|
154 |
case bg :: rest if is_control_block_pair(bg, sym) => open = rest |
de16d797adbe
more robust HTML output: non-balanced bsub/esub are shown verbatim, e.g. within mixfix declarations (due to extra markup);
wenzelm
parents:
73208
diff
changeset
|
155 |
case _ => ok = false |
de16d797adbe
more robust HTML output: non-balanced bsub/esub are shown verbatim, e.g. within mixfix declarations (due to extra markup);
wenzelm
parents:
73208
diff
changeset
|
156 |
} |
de16d797adbe
more robust HTML output: non-balanced bsub/esub are shown verbatim, e.g. within mixfix declarations (due to extra markup);
wenzelm
parents:
73208
diff
changeset
|
157 |
} |
de16d797adbe
more robust HTML output: non-balanced bsub/esub are shown verbatim, e.g. within mixfix declarations (due to extra markup);
wenzelm
parents:
73208
diff
changeset
|
158 |
} |
de16d797adbe
more robust HTML output: non-balanced bsub/esub are shown verbatim, e.g. within mixfix declarations (due to extra markup);
wenzelm
parents:
73208
diff
changeset
|
159 |
ok && open.isEmpty |
de16d797adbe
more robust HTML output: non-balanced bsub/esub are shown verbatim, e.g. within mixfix declarations (due to extra markup);
wenzelm
parents:
73208
diff
changeset
|
160 |
} |
de16d797adbe
more robust HTML output: non-balanced bsub/esub are shown verbatim, e.g. within mixfix declarations (due to extra markup);
wenzelm
parents:
73208
diff
changeset
|
161 |
|
75393 | 162 |
def output( |
163 |
s: StringBuilder, |
|
164 |
text: String, |
|
165 |
control_blocks: Boolean, |
|
166 |
hidden: Boolean, |
|
167 |
permissive: Boolean |
|
168 |
): Unit = { |
|
66018
9ce3720976dc
permissive output of XML.Text, e.g. relevant for embedded <style>;
wenzelm
parents:
66006
diff
changeset
|
169 |
def output_string(str: String): Unit = |
73204
aa3d4cf7825a
clarified signature: no symbol markup within XML attributes;
wenzelm
parents:
73203
diff
changeset
|
170 |
XML.output_string(s, str, permissive = permissive) |
66018
9ce3720976dc
permissive output of XML.Text, e.g. relevant for embedded <style>;
wenzelm
parents:
66006
diff
changeset
|
171 |
|
65997
e3dc9ea67a62
output control symbols like ML version, with optionally hidden source;
wenzelm
parents:
65993
diff
changeset
|
172 |
def output_hidden(body: => Unit): Unit = |
e3dc9ea67a62
output control symbols like ML version, with optionally hidden source;
wenzelm
parents:
65993
diff
changeset
|
173 |
if (hidden) { s ++= "<span class=\"hidden\">"; body; s ++= "</span>" } |
37200
0f3edc64356a
added HTML.encode (in Scala), similar to HTML.output in ML;
wenzelm
parents:
36016
diff
changeset
|
174 |
|
65997
e3dc9ea67a62
output control symbols like ML version, with optionally hidden source;
wenzelm
parents:
65993
diff
changeset
|
175 |
def output_symbol(sym: Symbol.Symbol): Unit = |
e3dc9ea67a62
output control symbols like ML version, with optionally hidden source;
wenzelm
parents:
65993
diff
changeset
|
176 |
if (sym != "") { |
73206 | 177 |
control_block_begin.get(sym) match { |
73209
de16d797adbe
more robust HTML output: non-balanced bsub/esub are shown verbatim, e.g. within mixfix declarations (due to extra markup);
wenzelm
parents:
73208
diff
changeset
|
178 |
case Some(op) if control_blocks => |
73206 | 179 |
output_hidden(output_string(sym)) |
180 |
XML.output_elem(s, Markup(op.name, Nil)) |
|
73209
de16d797adbe
more robust HTML output: non-balanced bsub/esub are shown verbatim, e.g. within mixfix declarations (due to extra markup);
wenzelm
parents:
73208
diff
changeset
|
181 |
case _ => |
73206 | 182 |
control_block_end.get(sym) match { |
73209
de16d797adbe
more robust HTML output: non-balanced bsub/esub are shown verbatim, e.g. within mixfix declarations (due to extra markup);
wenzelm
parents:
73208
diff
changeset
|
183 |
case Some(op) if control_blocks => |
73206 | 184 |
XML.output_elem_end(s, op.name) |
185 |
output_hidden(output_string(sym)) |
|
73209
de16d797adbe
more robust HTML output: non-balanced bsub/esub are shown verbatim, e.g. within mixfix declarations (due to extra markup);
wenzelm
parents:
73208
diff
changeset
|
186 |
case _ => |
73206 | 187 |
if (hidden && Symbol.is_control_encoded(sym)) { |
188 |
output_hidden(output_string(Symbol.control_prefix)) |
|
189 |
s ++= "<span class=\"control\">" |
|
190 |
output_string(Symbol.control_name(sym).get) |
|
191 |
s ++= "</span>" |
|
192 |
output_hidden(output_string(Symbol.control_suffix)) |
|
193 |
} |
|
194 |
else output_string(sym) |
|
67255
f1f983484878
HTML rendering of \<^control> as in Isabelle/jEdit;
wenzelm
parents:
66212
diff
changeset
|
195 |
} |
65997
e3dc9ea67a62
output control symbols like ML version, with optionally hidden source;
wenzelm
parents:
65993
diff
changeset
|
196 |
} |
e3dc9ea67a62
output control symbols like ML version, with optionally hidden source;
wenzelm
parents:
65993
diff
changeset
|
197 |
} |
59063 | 198 |
|
62104
fb73c0d7bb37
clarified symbol insertion, depending on buffer encoding;
wenzelm
parents:
60215
diff
changeset
|
199 |
var ctrl = "" |
59063 | 200 |
for (sym <- Symbol.iterator(text)) { |
65997
e3dc9ea67a62
output control symbols like ML version, with optionally hidden source;
wenzelm
parents:
65993
diff
changeset
|
201 |
if (is_control(sym)) { output_symbol(ctrl); ctrl = sym } |
59063 | 202 |
else { |
62104
fb73c0d7bb37
clarified symbol insertion, depending on buffer encoding;
wenzelm
parents:
60215
diff
changeset
|
203 |
control.get(ctrl) match { |
73206 | 204 |
case Some(op) if Symbol.is_controllable(sym) => |
65997
e3dc9ea67a62
output control symbols like ML version, with optionally hidden source;
wenzelm
parents:
65993
diff
changeset
|
205 |
output_hidden(output_symbol(ctrl)) |
73206 | 206 |
XML.output_elem(s, Markup(op.name, Nil)) |
65997
e3dc9ea67a62
output control symbols like ML version, with optionally hidden source;
wenzelm
parents:
65993
diff
changeset
|
207 |
output_symbol(sym) |
73206 | 208 |
XML.output_elem_end(s, op.name) |
59063 | 209 |
case _ => |
65997
e3dc9ea67a62
output control symbols like ML version, with optionally hidden source;
wenzelm
parents:
65993
diff
changeset
|
210 |
output_symbol(ctrl) |
e3dc9ea67a62
output control symbols like ML version, with optionally hidden source;
wenzelm
parents:
65993
diff
changeset
|
211 |
output_symbol(sym) |
59063 | 212 |
} |
62104
fb73c0d7bb37
clarified symbol insertion, depending on buffer encoding;
wenzelm
parents:
60215
diff
changeset
|
213 |
ctrl = "" |
59063 | 214 |
} |
37200
0f3edc64356a
added HTML.encode (in Scala), similar to HTML.output in ML;
wenzelm
parents:
36016
diff
changeset
|
215 |
} |
65997
e3dc9ea67a62
output control symbols like ML version, with optionally hidden source;
wenzelm
parents:
65993
diff
changeset
|
216 |
output_symbol(ctrl) |
64355 | 217 |
} |
59063 | 218 |
|
75393 | 219 |
def output(text: String): String = { |
73209
de16d797adbe
more robust HTML output: non-balanced bsub/esub are shown verbatim, e.g. within mixfix declarations (due to extra markup);
wenzelm
parents:
73208
diff
changeset
|
220 |
val control_blocks = check_control_blocks(List(XML.Text(text))) |
de16d797adbe
more robust HTML output: non-balanced bsub/esub are shown verbatim, e.g. within mixfix declarations (due to extra markup);
wenzelm
parents:
73208
diff
changeset
|
221 |
Library.make_string(output(_, text, |
de16d797adbe
more robust HTML output: non-balanced bsub/esub are shown verbatim, e.g. within mixfix declarations (due to extra markup);
wenzelm
parents:
73208
diff
changeset
|
222 |
control_blocks = control_blocks, hidden = false, permissive = true)) |
de16d797adbe
more robust HTML output: non-balanced bsub/esub are shown verbatim, e.g. within mixfix declarations (due to extra markup);
wenzelm
parents:
73208
diff
changeset
|
223 |
} |
64355 | 224 |
|
225 |
||
226 |
/* output XML as HTML */ |
|
227 |
||
65834
67a6e0f166c2
extra space only for some structual elements, but not <a>, <b>, <em> etc. (amending 8a0fe5469ba0);
wenzelm
parents:
65773
diff
changeset
|
228 |
private val structural_elements = |
67a6e0f166c2
extra space only for some structual elements, but not <a>, <b>, <em> etc. (amending 8a0fe5469ba0);
wenzelm
parents:
65773
diff
changeset
|
229 |
Set("head", "body", "meta", "div", "pre", "p", "title", "h1", "h2", "h3", "h4", "h5", "h6", |
67a6e0f166c2
extra space only for some structual elements, but not <a>, <b>, <em> etc. (amending 8a0fe5469ba0);
wenzelm
parents:
65773
diff
changeset
|
230 |
"ul", "ol", "dl", "li", "dt", "dd") |
67a6e0f166c2
extra space only for some structual elements, but not <a>, <b>, <em> etc. (amending 8a0fe5469ba0);
wenzelm
parents:
65773
diff
changeset
|
231 |
|
75393 | 232 |
def output(s: StringBuilder, xml: XML.Body, hidden: Boolean, structural: Boolean): Unit = { |
233 |
def output_body(body: XML.Body): Unit = { |
|
73209
de16d797adbe
more robust HTML output: non-balanced bsub/esub are shown verbatim, e.g. within mixfix declarations (due to extra markup);
wenzelm
parents:
73208
diff
changeset
|
234 |
val control_blocks = check_control_blocks(body) |
73205 | 235 |
body foreach { |
64355 | 236 |
case XML.Elem(markup, Nil) => |
73204
aa3d4cf7825a
clarified signature: no symbol markup within XML attributes;
wenzelm
parents:
73203
diff
changeset
|
237 |
XML.output_elem(s, markup, end = true) |
64355 | 238 |
case XML.Elem(markup, ts) => |
67337
4254cfd15b00
more tight HTML output: avoid extra lines within <pre>;
wenzelm
parents:
67336
diff
changeset
|
239 |
if (structural && structural_elements(markup.name)) s += '\n' |
73204
aa3d4cf7825a
clarified signature: no symbol markup within XML attributes;
wenzelm
parents:
73203
diff
changeset
|
240 |
XML.output_elem(s, markup) |
73205 | 241 |
output_body(ts) |
73204
aa3d4cf7825a
clarified signature: no symbol markup within XML attributes;
wenzelm
parents:
73203
diff
changeset
|
242 |
XML.output_elem_end(s, markup.name) |
67337
4254cfd15b00
more tight HTML output: avoid extra lines within <pre>;
wenzelm
parents:
67336
diff
changeset
|
243 |
if (structural && structural_elements(markup.name)) s += '\n' |
65997
e3dc9ea67a62
output control symbols like ML version, with optionally hidden source;
wenzelm
parents:
65993
diff
changeset
|
244 |
case XML.Text(txt) => |
73209
de16d797adbe
more robust HTML output: non-balanced bsub/esub are shown verbatim, e.g. within mixfix declarations (due to extra markup);
wenzelm
parents:
73208
diff
changeset
|
245 |
output(s, txt, control_blocks = control_blocks, hidden = hidden, permissive = true) |
64355 | 246 |
} |
73205 | 247 |
} |
248 |
output_body(xml) |
|
37200
0f3edc64356a
added HTML.encode (in Scala), similar to HTML.output in ML;
wenzelm
parents:
36016
diff
changeset
|
249 |
} |
0f3edc64356a
added HTML.encode (in Scala), similar to HTML.output in ML;
wenzelm
parents:
36016
diff
changeset
|
250 |
|
67337
4254cfd15b00
more tight HTML output: avoid extra lines within <pre>;
wenzelm
parents:
67336
diff
changeset
|
251 |
def output(body: XML.Body, hidden: Boolean, structural: Boolean): String = |
74794
c606fddc5b05
slightly faster XML output: avoid too much regrowing of StringBuilder;
wenzelm
parents:
74754
diff
changeset
|
252 |
Library.make_string(output(_, body, hidden, structural), capacity = XML.text_length(body) * 2) |
65997
e3dc9ea67a62
output control symbols like ML version, with optionally hidden source;
wenzelm
parents:
65993
diff
changeset
|
253 |
|
67337
4254cfd15b00
more tight HTML output: avoid extra lines within <pre>;
wenzelm
parents:
67336
diff
changeset
|
254 |
def output(tree: XML.Tree, hidden: Boolean, structural: Boolean): String = |
4254cfd15b00
more tight HTML output: avoid extra lines within <pre>;
wenzelm
parents:
67336
diff
changeset
|
255 |
output(List(tree), hidden, structural) |
64355 | 256 |
|
257 |
||
74921 | 258 |
/* input text */ |
259 |
||
260 |
def input(text: String): String = |
|
261 |
org.apache.commons.text.StringEscapeUtils.unescapeHtml4(text) |
|
262 |
||
263 |
||
65892 | 264 |
/* messages */ |
265 |
||
65939 | 266 |
// background |
65993 | 267 |
val writeln_message: Attribute = class_("writeln_message") |
268 |
val warning_message: Attribute = class_("warning_message") |
|
269 |
val error_message: Attribute = class_("error_message") |
|
65892 | 270 |
|
65939 | 271 |
// underline |
65993 | 272 |
val writeln: Attribute = class_("writeln") |
273 |
val warning: Attribute = class_("warning") |
|
274 |
val error: Attribute = class_("error") |
|
65892 | 275 |
|
65944 | 276 |
|
277 |
/* tooltips */ |
|
278 |
||
279 |
def tooltip(item: XML.Body, tip: XML.Body): XML.Elem = |
|
65992 | 280 |
span(item ::: List(div("tooltip", tip))) |
65944 | 281 |
|
282 |
def tooltip_errors(item: XML.Body, msgs: List[XML.Body]): XML.Elem = |
|
283 |
HTML.error(tooltip(item, msgs.map(msg => error_message(pre(msg))))) |
|
65892 | 284 |
|
285 |
||
66196 | 286 |
/* GUI elements */ |
287 |
||
75393 | 288 |
object GUI { |
66196 | 289 |
private def optional_value(text: String): XML.Attributes = |
290 |
proper_string(text).map(a => "value" -> a).toList |
|
291 |
||
292 |
private def optional_name(name: String): XML.Attributes = |
|
293 |
proper_string(name).map(a => "name" -> a).toList |
|
294 |
||
295 |
private def optional_title(tooltip: String): XML.Attributes = |
|
296 |
proper_string(tooltip).map(a => "title" -> a).toList |
|
297 |
||
298 |
private def optional_submit(submit: Boolean): XML.Attributes = |
|
299 |
if (submit) List("onChange" -> "this.form.submit()") else Nil |
|
300 |
||
301 |
private def optional_checked(selected: Boolean): XML.Attributes = |
|
302 |
if (selected) List("checked" -> "") else Nil |
|
303 |
||
304 |
private def optional_action(action: String): XML.Attributes = |
|
305 |
proper_string(action).map(a => "action" -> a).toList |
|
306 |
||
66210 | 307 |
private def optional_onclick(script: String): XML.Attributes = |
308 |
proper_string(script).map(a => "onclick" -> a).toList |
|
309 |
||
310 |
private def optional_onchange(script: String): XML.Attributes = |
|
311 |
proper_string(script).map(a => "onchange" -> a).toList |
|
312 |
||
313 |
def button(body: XML.Body, name: String = "", tooltip: String = "", submit: Boolean = false, |
|
314 |
script: String = ""): XML.Elem = |
|
66196 | 315 |
XML.Elem( |
316 |
Markup("button", |
|
317 |
List("type" -> (if (submit) "submit" else "button"), "value" -> "true") ::: |
|
66210 | 318 |
optional_name(name) ::: optional_title(tooltip) ::: optional_onclick(script)), body) |
66196 | 319 |
|
320 |
def checkbox(body: XML.Body, name: String = "", tooltip: String = "", submit: Boolean = false, |
|
66210 | 321 |
selected: Boolean = false, script: String = ""): XML.Elem = |
66196 | 322 |
XML.elem("label", |
323 |
XML.elem( |
|
324 |
Markup("input", |
|
325 |
List("type" -> "checkbox", "value" -> "true") ::: optional_name(name) ::: |
|
326 |
optional_title(tooltip) ::: optional_submit(submit) ::: |
|
66210 | 327 |
optional_checked(selected) ::: optional_onchange(script))) :: body) |
66196 | 328 |
|
329 |
def text_field(columns: Int = 0, text: String = "", name: String = "", tooltip: String = "", |
|
66210 | 330 |
submit: Boolean = false, script: String = ""): XML.Elem = |
66196 | 331 |
XML.elem(Markup("input", |
332 |
List("type" -> "text") ::: |
|
333 |
(if (columns > 0) List("size" -> columns.toString) else Nil) ::: |
|
66210 | 334 |
optional_value(text) ::: optional_name(name) ::: optional_title(tooltip) ::: |
335 |
optional_submit(submit) ::: optional_onchange(script))) |
|
66196 | 336 |
|
337 |
def parameter(text: String = "", name: String = ""): XML.Elem = |
|
338 |
XML.elem( |
|
339 |
Markup("input", List("type" -> "hidden") ::: optional_value(text) ::: optional_name(name))) |
|
340 |
||
66209 | 341 |
def form(body: XML.Body, name: String = "", action: String = "", http_post: Boolean = false) |
342 |
: XML.Elem = |
|
343 |
XML.Elem( |
|
344 |
Markup("form", optional_name(name) ::: optional_action(action) ::: |
|
345 |
(if (http_post) List("method" -> "post") else Nil)), body) |
|
66196 | 346 |
} |
347 |
||
348 |
||
66200 | 349 |
/* GUI layout */ |
350 |
||
75393 | 351 |
object Wrap_Panel { |
352 |
object Alignment extends Enumeration { |
|
66200 | 353 |
val left, right, center = Value |
354 |
} |
|
355 |
||
75393 | 356 |
def apply( |
357 |
contents: List[XML.Elem], |
|
358 |
name: String = "", |
|
359 |
action: String = "", |
|
360 |
alignment: Alignment.Value = Alignment.right |
|
361 |
): XML.Elem = { |
|
66200 | 362 |
val body = Library.separate(XML.Text(" "), contents) |
363 |
GUI.form(List(div(body) + ("style" -> ("text-align: " + alignment))), |
|
364 |
name = name, action = action) |
|
365 |
} |
|
366 |
} |
|
367 |
||
368 |
||
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
50707
diff
changeset
|
369 |
/* document */ |
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
50707
diff
changeset
|
370 |
|
64359 | 371 |
val header: String = |
69804 | 372 |
XML.header + |
373 |
"""<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd"> |
|
64359 | 374 |
<html xmlns="http://www.w3.org/1999/xhtml">""" |
375 |
||
73129 | 376 |
val footer: String = """</html>""" |
377 |
||
64359 | 378 |
val head_meta: XML.Elem = |
379 |
XML.Elem(Markup("meta", |
|
380 |
List("http-equiv" -> "Content-Type", "content" -> "text/html; charset=utf-8")), Nil) |
|
381 |
||
75393 | 382 |
def output_document( |
383 |
head: XML.Body, |
|
384 |
body: XML.Body, |
|
67337
4254cfd15b00
more tight HTML output: avoid extra lines within <pre>;
wenzelm
parents:
67336
diff
changeset
|
385 |
css: String = "isabelle.css", |
4254cfd15b00
more tight HTML output: avoid extra lines within <pre>;
wenzelm
parents:
67336
diff
changeset
|
386 |
hidden: Boolean = true, |
75393 | 387 |
structural: Boolean = true |
388 |
): String = { |
|
64359 | 389 |
cat_lines( |
73129 | 390 |
List( |
391 |
header, |
|
65997
e3dc9ea67a62
output control symbols like ML version, with optionally hidden source;
wenzelm
parents:
65993
diff
changeset
|
392 |
output( |
66000 | 393 |
XML.elem("head", head_meta :: (if (css == "") Nil else List(style_file(css))) ::: head), |
67337
4254cfd15b00
more tight HTML output: avoid extra lines within <pre>;
wenzelm
parents:
67336
diff
changeset
|
394 |
hidden = hidden, structural = structural), |
4254cfd15b00
more tight HTML output: avoid extra lines within <pre>;
wenzelm
parents:
67336
diff
changeset
|
395 |
output(XML.elem("body", body), |
73129 | 396 |
hidden = hidden, structural = structural), |
397 |
footer)) |
|
65997
e3dc9ea67a62
output control symbols like ML version, with optionally hidden source;
wenzelm
parents:
65993
diff
changeset
|
398 |
} |
64359 | 399 |
|
65838 | 400 |
|
66000 | 401 |
/* fonts */ |
402 |
||
74709 | 403 |
val fonts_path: Path = Path.explode("fonts") |
404 |
||
75393 | 405 |
def init_fonts(dir: Path): Unit = { |
74709 | 406 |
val fonts_dir = Isabelle_System.make_directory(dir + HTML.fonts_path) |
407 |
for (entry <- Isabelle_Fonts.fonts(hidden = true)) |
|
408 |
Isabelle_System.copy_file(entry.path, fonts_dir) |
|
409 |
} |
|
410 |
||
411 |
def fonts_dir(prefix: String)(ttf_name: String): String = prefix + "/" + ttf_name |
|
412 |
||
66000 | 413 |
def fonts_url(): String => String = |
69374 | 414 |
(for (entry <- Isabelle_Fonts.fonts(hidden = true)) |
70743
342b0a1fc86d
proper file name instead of font name (amending dc9a39c3f75d);
wenzelm
parents:
69804
diff
changeset
|
415 |
yield (entry.path.file_name -> Url.print_file(entry.path.file))).toMap |
66000 | 416 |
|
75393 | 417 |
def fonts_css(make_url: String => String = fonts_url()): String = { |
69360 | 418 |
def font_face(entry: Isabelle_Fonts.Entry): String = |
66000 | 419 |
cat_lines( |
420 |
List( |
|
421 |
"@font-face {", |
|
69360 | 422 |
" font-family: '" + entry.family + "';", |
69366 | 423 |
" src: url('" + make_url(entry.path.file_name) + "') format('truetype');") ::: |
69360 | 424 |
(if (entry.is_bold) List(" font-weight: bold;") else Nil) ::: |
425 |
(if (entry.is_italic) List(" font-style: italic;") else Nil) ::: |
|
66000 | 426 |
List("}")) |
427 |
||
71601 | 428 |
("/* Isabelle fonts */" :: Isabelle_Fonts.fonts(hidden = true).map(font_face)) |
69362 | 429 |
.mkString("", "\n\n", "\n") |
66000 | 430 |
} |
431 |
||
75393 | 432 |
def fonts_css_dir(prefix: String = ""): String = { |
74709 | 433 |
val prefix1 = if (prefix.isEmpty || prefix.endsWith("/")) prefix else prefix + "/" |
434 |
fonts_css(fonts_dir(prefix1 + fonts_path.implode)) |
|
435 |
} |
|
66000 | 436 |
|
74709 | 437 |
|
438 |
/* document directory context (fonts + css) */ |
|
439 |
||
65998 | 440 |
def isabelle_css: Path = Path.explode("~~/etc/isabelle.css") |
441 |
||
65838 | 442 |
def write_document(dir: Path, name: String, head: XML.Body, body: XML.Body, |
74709 | 443 |
base: Option[Path] = None, |
69366 | 444 |
css: String = isabelle_css.file_name, |
67337
4254cfd15b00
more tight HTML output: avoid extra lines within <pre>;
wenzelm
parents:
67336
diff
changeset
|
445 |
hidden: Boolean = true, |
75393 | 446 |
structural: Boolean = true |
447 |
): Unit = { |
|
74709 | 448 |
Isabelle_System.make_directory(dir) |
75938
17d51bdabded
proper fonts_prefix (amending c14409948063): default is "" due to self-cancellation of dir;
wenzelm
parents:
75933
diff
changeset
|
449 |
val fonts_prefix = relative_href(base getOrElse dir, base = Some(dir)) |
17d51bdabded
proper fonts_prefix (amending c14409948063): default is "" due to self-cancellation of dir;
wenzelm
parents:
75933
diff
changeset
|
450 |
val fonts = fonts_css_dir(fonts_prefix) |
75933 | 451 |
File.write(dir + isabelle_css.base, fonts + "\n\n" + File.read(isabelle_css)) |
67337
4254cfd15b00
more tight HTML output: avoid extra lines within <pre>;
wenzelm
parents:
67336
diff
changeset
|
452 |
File.write(dir + Path.basic(name), |
4254cfd15b00
more tight HTML output: avoid extra lines within <pre>;
wenzelm
parents:
67336
diff
changeset
|
453 |
output_document(head, body, css = css, hidden = hidden, structural = structural)) |
65838 | 454 |
} |
33984 | 455 |
} |