author | wenzelm |
Fri, 22 Dec 2017 15:49:44 +0100 | |
changeset 67255 | f1f983484878 |
parent 66212 | f41396c15bb1 |
child 67336 | 3ee6da378183 |
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 |
|
33984 | 10 |
object HTML |
11 |
{ |
|
65997
e3dc9ea67a62
output control symbols like ML version, with optionally hidden source;
wenzelm
parents:
65993
diff
changeset
|
12 |
/* output text with control symbols */ |
59063 | 13 |
|
65997
e3dc9ea67a62
output control symbols like ML version, with optionally hidden source;
wenzelm
parents:
65993
diff
changeset
|
14 |
private val control = |
e3dc9ea67a62
output control symbols like ML version, with optionally hidden source;
wenzelm
parents:
65993
diff
changeset
|
15 |
Map( |
e3dc9ea67a62
output control symbols like ML version, with optionally hidden source;
wenzelm
parents:
65993
diff
changeset
|
16 |
Symbol.sub -> "sub", Symbol.sub_decoded -> "sub", |
e3dc9ea67a62
output control symbols like ML version, with optionally hidden source;
wenzelm
parents:
65993
diff
changeset
|
17 |
Symbol.sup -> "sup", Symbol.sup_decoded -> "sup", |
e3dc9ea67a62
output control symbols like ML version, with optionally hidden source;
wenzelm
parents:
65993
diff
changeset
|
18 |
Symbol.bold -> "b", Symbol.bold_decoded -> "b") |
e3dc9ea67a62
output control symbols like ML version, with optionally hidden source;
wenzelm
parents:
65993
diff
changeset
|
19 |
|
e3dc9ea67a62
output control symbols like ML version, with optionally hidden source;
wenzelm
parents:
65993
diff
changeset
|
20 |
private val control_block = |
62104
fb73c0d7bb37
clarified symbol insertion, depending on buffer encoding;
wenzelm
parents:
60215
diff
changeset
|
21 |
Map( |
65997
e3dc9ea67a62
output control symbols like ML version, with optionally hidden source;
wenzelm
parents:
65993
diff
changeset
|
22 |
Symbol.bsub -> "<sub>", Symbol.bsub_decoded -> "<sub>", |
e3dc9ea67a62
output control symbols like ML version, with optionally hidden source;
wenzelm
parents:
65993
diff
changeset
|
23 |
Symbol.esub -> "</sub>", Symbol.esub_decoded -> "</sub>", |
e3dc9ea67a62
output control symbols like ML version, with optionally hidden source;
wenzelm
parents:
65993
diff
changeset
|
24 |
Symbol.bsup -> "<sup>", Symbol.bsup_decoded -> "<sup>", |
e3dc9ea67a62
output control symbols like ML version, with optionally hidden source;
wenzelm
parents:
65993
diff
changeset
|
25 |
Symbol.esup -> "</sup>", Symbol.esup_decoded -> "</sup>") |
e3dc9ea67a62
output control symbols like ML version, with optionally hidden source;
wenzelm
parents:
65993
diff
changeset
|
26 |
|
e3dc9ea67a62
output control symbols like ML version, with optionally hidden source;
wenzelm
parents:
65993
diff
changeset
|
27 |
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
|
28 |
|
66018
9ce3720976dc
permissive output of XML.Text, e.g. relevant for embedded <style>;
wenzelm
parents:
66006
diff
changeset
|
29 |
def output_char_permissive(c: Char, s: StringBuilder) |
65997
e3dc9ea67a62
output control symbols like ML version, with optionally hidden source;
wenzelm
parents:
65993
diff
changeset
|
30 |
{ |
66018
9ce3720976dc
permissive output of XML.Text, e.g. relevant for embedded <style>;
wenzelm
parents:
66006
diff
changeset
|
31 |
c match { |
9ce3720976dc
permissive output of XML.Text, e.g. relevant for embedded <style>;
wenzelm
parents:
66006
diff
changeset
|
32 |
case '<' => s ++= "<" |
9ce3720976dc
permissive output of XML.Text, e.g. relevant for embedded <style>;
wenzelm
parents:
66006
diff
changeset
|
33 |
case '>' => s ++= ">" |
9ce3720976dc
permissive output of XML.Text, e.g. relevant for embedded <style>;
wenzelm
parents:
66006
diff
changeset
|
34 |
case '&' => s ++= "&" |
9ce3720976dc
permissive output of XML.Text, e.g. relevant for embedded <style>;
wenzelm
parents:
66006
diff
changeset
|
35 |
case _ => s += c |
9ce3720976dc
permissive output of XML.Text, e.g. relevant for embedded <style>;
wenzelm
parents:
66006
diff
changeset
|
36 |
} |
9ce3720976dc
permissive output of XML.Text, e.g. relevant for embedded <style>;
wenzelm
parents:
66006
diff
changeset
|
37 |
} |
9ce3720976dc
permissive output of XML.Text, e.g. relevant for embedded <style>;
wenzelm
parents:
66006
diff
changeset
|
38 |
|
9ce3720976dc
permissive output of XML.Text, e.g. relevant for embedded <style>;
wenzelm
parents:
66006
diff
changeset
|
39 |
def output(text: String, s: StringBuilder, hidden: Boolean, permissive: Boolean) |
9ce3720976dc
permissive output of XML.Text, e.g. relevant for embedded <style>;
wenzelm
parents:
66006
diff
changeset
|
40 |
{ |
9ce3720976dc
permissive output of XML.Text, e.g. relevant for embedded <style>;
wenzelm
parents:
66006
diff
changeset
|
41 |
def output_char(c: Char): Unit = |
9ce3720976dc
permissive output of XML.Text, e.g. relevant for embedded <style>;
wenzelm
parents:
66006
diff
changeset
|
42 |
if (permissive) output_char_permissive(c, s) |
9ce3720976dc
permissive output of XML.Text, e.g. relevant for embedded <style>;
wenzelm
parents:
66006
diff
changeset
|
43 |
else XML.output_char(c, s) |
9ce3720976dc
permissive output of XML.Text, e.g. relevant for embedded <style>;
wenzelm
parents:
66006
diff
changeset
|
44 |
|
9ce3720976dc
permissive output of XML.Text, e.g. relevant for embedded <style>;
wenzelm
parents:
66006
diff
changeset
|
45 |
def output_string(str: String): Unit = |
9ce3720976dc
permissive output of XML.Text, e.g. relevant for embedded <style>;
wenzelm
parents:
66006
diff
changeset
|
46 |
str.iterator.foreach(output_char) |
9ce3720976dc
permissive output of XML.Text, e.g. relevant for embedded <style>;
wenzelm
parents:
66006
diff
changeset
|
47 |
|
65997
e3dc9ea67a62
output control symbols like ML version, with optionally hidden source;
wenzelm
parents:
65993
diff
changeset
|
48 |
def output_hidden(body: => Unit): Unit = |
e3dc9ea67a62
output control symbols like ML version, with optionally hidden source;
wenzelm
parents:
65993
diff
changeset
|
49 |
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
|
50 |
|
65997
e3dc9ea67a62
output control symbols like ML version, with optionally hidden source;
wenzelm
parents:
65993
diff
changeset
|
51 |
def output_symbol(sym: Symbol.Symbol): Unit = |
e3dc9ea67a62
output control symbols like ML version, with optionally hidden source;
wenzelm
parents:
65993
diff
changeset
|
52 |
if (sym != "") { |
e3dc9ea67a62
output control symbols like ML version, with optionally hidden source;
wenzelm
parents:
65993
diff
changeset
|
53 |
control_block.get(sym) match { |
e3dc9ea67a62
output control symbols like ML version, with optionally hidden source;
wenzelm
parents:
65993
diff
changeset
|
54 |
case Some(html) if html.startsWith("</") => |
66018
9ce3720976dc
permissive output of XML.Text, e.g. relevant for embedded <style>;
wenzelm
parents:
66006
diff
changeset
|
55 |
s ++= html; output_hidden(output_string(sym)) |
65997
e3dc9ea67a62
output control symbols like ML version, with optionally hidden source;
wenzelm
parents:
65993
diff
changeset
|
56 |
case Some(html) => |
66018
9ce3720976dc
permissive output of XML.Text, e.g. relevant for embedded <style>;
wenzelm
parents:
66006
diff
changeset
|
57 |
output_hidden(output_string(sym)); s ++= html |
65997
e3dc9ea67a62
output control symbols like ML version, with optionally hidden source;
wenzelm
parents:
65993
diff
changeset
|
58 |
case None => |
67255
f1f983484878
HTML rendering of \<^control> as in Isabelle/jEdit;
wenzelm
parents:
66212
diff
changeset
|
59 |
if (hidden && Symbol.is_control_encoded(sym)) { |
f1f983484878
HTML rendering of \<^control> as in Isabelle/jEdit;
wenzelm
parents:
66212
diff
changeset
|
60 |
output_hidden(output_string(Symbol.control_prefix)) |
f1f983484878
HTML rendering of \<^control> as in Isabelle/jEdit;
wenzelm
parents:
66212
diff
changeset
|
61 |
s ++= "<span class=\"control\">" |
f1f983484878
HTML rendering of \<^control> as in Isabelle/jEdit;
wenzelm
parents:
66212
diff
changeset
|
62 |
output_string(Symbol.control_name(sym).get) |
f1f983484878
HTML rendering of \<^control> as in Isabelle/jEdit;
wenzelm
parents:
66212
diff
changeset
|
63 |
s ++= "</span>" |
f1f983484878
HTML rendering of \<^control> as in Isabelle/jEdit;
wenzelm
parents:
66212
diff
changeset
|
64 |
output_hidden(output_string(Symbol.control_suffix)) |
f1f983484878
HTML rendering of \<^control> as in Isabelle/jEdit;
wenzelm
parents:
66212
diff
changeset
|
65 |
} |
f1f983484878
HTML rendering of \<^control> as in Isabelle/jEdit;
wenzelm
parents:
66212
diff
changeset
|
66 |
else output_string(sym) |
65997
e3dc9ea67a62
output control symbols like ML version, with optionally hidden source;
wenzelm
parents:
65993
diff
changeset
|
67 |
} |
e3dc9ea67a62
output control symbols like ML version, with optionally hidden source;
wenzelm
parents:
65993
diff
changeset
|
68 |
} |
59063 | 69 |
|
62104
fb73c0d7bb37
clarified symbol insertion, depending on buffer encoding;
wenzelm
parents:
60215
diff
changeset
|
70 |
var ctrl = "" |
59063 | 71 |
for (sym <- Symbol.iterator(text)) { |
65997
e3dc9ea67a62
output control symbols like ML version, with optionally hidden source;
wenzelm
parents:
65993
diff
changeset
|
72 |
if (is_control(sym)) { output_symbol(ctrl); ctrl = sym } |
59063 | 73 |
else { |
62104
fb73c0d7bb37
clarified symbol insertion, depending on buffer encoding;
wenzelm
parents:
60215
diff
changeset
|
74 |
control.get(ctrl) match { |
66006
cec184536dfd
uniform notion of Symbol.is_controllable (see also 265d9300d523);
wenzelm
parents:
66001
diff
changeset
|
75 |
case Some(elem) if Symbol.is_controllable(sym) => |
65997
e3dc9ea67a62
output control symbols like ML version, with optionally hidden source;
wenzelm
parents:
65993
diff
changeset
|
76 |
output_hidden(output_symbol(ctrl)) |
65991 | 77 |
s += '<'; s ++= elem; s += '>' |
65997
e3dc9ea67a62
output control symbols like ML version, with optionally hidden source;
wenzelm
parents:
65993
diff
changeset
|
78 |
output_symbol(sym) |
65991 | 79 |
s ++= "</"; s ++= elem; s += '>' |
59063 | 80 |
case _ => |
65997
e3dc9ea67a62
output control symbols like ML version, with optionally hidden source;
wenzelm
parents:
65993
diff
changeset
|
81 |
output_symbol(ctrl) |
e3dc9ea67a62
output control symbols like ML version, with optionally hidden source;
wenzelm
parents:
65993
diff
changeset
|
82 |
output_symbol(sym) |
59063 | 83 |
} |
62104
fb73c0d7bb37
clarified symbol insertion, depending on buffer encoding;
wenzelm
parents:
60215
diff
changeset
|
84 |
ctrl = "" |
59063 | 85 |
} |
37200
0f3edc64356a
added HTML.encode (in Scala), similar to HTML.output in ML;
wenzelm
parents:
36016
diff
changeset
|
86 |
} |
65997
e3dc9ea67a62
output control symbols like ML version, with optionally hidden source;
wenzelm
parents:
65993
diff
changeset
|
87 |
output_symbol(ctrl) |
64355 | 88 |
} |
59063 | 89 |
|
66018
9ce3720976dc
permissive output of XML.Text, e.g. relevant for embedded <style>;
wenzelm
parents:
66006
diff
changeset
|
90 |
def output(text: String): String = |
9ce3720976dc
permissive output of XML.Text, e.g. relevant for embedded <style>;
wenzelm
parents:
66006
diff
changeset
|
91 |
Library.make_string(output(text, _, hidden = false, permissive = true)) |
64355 | 92 |
|
93 |
||
94 |
/* output XML as HTML */ |
|
95 |
||
65834
67a6e0f166c2
extra space only for some structual elements, but not <a>, <b>, <em> etc. (amending 8a0fe5469ba0);
wenzelm
parents:
65773
diff
changeset
|
96 |
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
|
97 |
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
|
98 |
"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
|
99 |
|
65997
e3dc9ea67a62
output control symbols like ML version, with optionally hidden source;
wenzelm
parents:
65993
diff
changeset
|
100 |
def output(body: XML.Body, s: StringBuilder, hidden: Boolean) |
64355 | 101 |
{ |
65991 | 102 |
def elem(markup: Markup) |
103 |
{ |
|
104 |
s ++= markup.name |
|
105 |
for ((a, b) <- markup.properties) { |
|
66018
9ce3720976dc
permissive output of XML.Text, e.g. relevant for embedded <style>;
wenzelm
parents:
66006
diff
changeset
|
106 |
s += ' ' |
9ce3720976dc
permissive output of XML.Text, e.g. relevant for embedded <style>;
wenzelm
parents:
66006
diff
changeset
|
107 |
s ++= a |
9ce3720976dc
permissive output of XML.Text, e.g. relevant for embedded <style>;
wenzelm
parents:
66006
diff
changeset
|
108 |
s += '=' |
9ce3720976dc
permissive output of XML.Text, e.g. relevant for embedded <style>;
wenzelm
parents:
66006
diff
changeset
|
109 |
s += '"' |
9ce3720976dc
permissive output of XML.Text, e.g. relevant for embedded <style>;
wenzelm
parents:
66006
diff
changeset
|
110 |
output(b, s, hidden = hidden, permissive = false) |
9ce3720976dc
permissive output of XML.Text, e.g. relevant for embedded <style>;
wenzelm
parents:
66006
diff
changeset
|
111 |
s += '"' |
65991 | 112 |
} |
113 |
} |
|
64355 | 114 |
def tree(t: XML.Tree): Unit = |
115 |
t match { |
|
116 |
case XML.Elem(markup, Nil) => |
|
65991 | 117 |
s += '<'; elem(markup); s ++= "/>" |
64355 | 118 |
case XML.Elem(markup, ts) => |
65834
67a6e0f166c2
extra space only for some structual elements, but not <a>, <b>, <em> etc. (amending 8a0fe5469ba0);
wenzelm
parents:
65773
diff
changeset
|
119 |
if (structural_elements(markup.name)) s += '\n' |
65991 | 120 |
s += '<'; elem(markup); s += '>' |
64355 | 121 |
ts.foreach(tree) |
65991 | 122 |
s ++= "</"; s ++= markup.name; s += '>' |
65834
67a6e0f166c2
extra space only for some structual elements, but not <a>, <b>, <em> etc. (amending 8a0fe5469ba0);
wenzelm
parents:
65773
diff
changeset
|
123 |
if (structural_elements(markup.name)) s += '\n' |
65997
e3dc9ea67a62
output control symbols like ML version, with optionally hidden source;
wenzelm
parents:
65993
diff
changeset
|
124 |
case XML.Text(txt) => |
66018
9ce3720976dc
permissive output of XML.Text, e.g. relevant for embedded <style>;
wenzelm
parents:
66006
diff
changeset
|
125 |
output(txt, s, hidden = hidden, permissive = true) |
64355 | 126 |
} |
127 |
body.foreach(tree) |
|
37200
0f3edc64356a
added HTML.encode (in Scala), similar to HTML.output in ML;
wenzelm
parents:
36016
diff
changeset
|
128 |
} |
0f3edc64356a
added HTML.encode (in Scala), similar to HTML.output in ML;
wenzelm
parents:
36016
diff
changeset
|
129 |
|
65997
e3dc9ea67a62
output control symbols like ML version, with optionally hidden source;
wenzelm
parents:
65993
diff
changeset
|
130 |
def output(body: XML.Body, hidden: Boolean): String = |
e3dc9ea67a62
output control symbols like ML version, with optionally hidden source;
wenzelm
parents:
65993
diff
changeset
|
131 |
Library.make_string(output(body, _, hidden)) |
e3dc9ea67a62
output control symbols like ML version, with optionally hidden source;
wenzelm
parents:
65993
diff
changeset
|
132 |
|
e3dc9ea67a62
output control symbols like ML version, with optionally hidden source;
wenzelm
parents:
65993
diff
changeset
|
133 |
def output(tree: XML.Tree, hidden: Boolean): String = |
e3dc9ea67a62
output control symbols like ML version, with optionally hidden source;
wenzelm
parents:
65993
diff
changeset
|
134 |
output(List(tree), hidden) |
64355 | 135 |
|
136 |
||
65753 | 137 |
/* attributes */ |
138 |
||
65992 | 139 |
class Attribute(val name: String, value: String) |
140 |
{ |
|
141 |
def xml: XML.Attribute = name -> value |
|
142 |
def apply(elem: XML.Elem): XML.Elem = elem + xml |
|
143 |
} |
|
65942 | 144 |
|
65992 | 145 |
def id(s: String): Attribute = new Attribute("id", s) |
65993 | 146 |
def class_(name: String): Attribute = new Attribute("class", name) |
65946 | 147 |
|
65992 | 148 |
def width(w: Int): Attribute = new Attribute("width", w.toString) |
149 |
def height(h: Int): Attribute = new Attribute("height", h.toString) |
|
65946 | 150 |
def size(w: Int, h: Int)(elem: XML.Elem): XML.Elem = width(w)(height(h)(elem)) |
65753 | 151 |
|
152 |
||
64359 | 153 |
/* structured markup operators */ |
154 |
||
155 |
def text(txt: String): XML.Body = if (txt.isEmpty) Nil else List(XML.Text(txt)) |
|
65753 | 156 |
val break: XML.Body = List(XML.elem("br")) |
64359 | 157 |
|
65992 | 158 |
class Operator(val name: String) |
159 |
{ |
|
160 |
def apply(body: XML.Body): XML.Elem = XML.elem(name, body) |
|
161 |
def apply(att: Attribute, body: XML.Body): XML.Elem = att(apply(body)) |
|
65993 | 162 |
def apply(c: String, body: XML.Body): XML.Elem = apply(class_(c), body) |
65992 | 163 |
} |
64356 | 164 |
|
64359 | 165 |
class Heading(name: String) extends Operator(name) |
65992 | 166 |
{ |
167 |
def apply(txt: String): XML.Elem = super.apply(text(txt)) |
|
168 |
def apply(att: Attribute, txt: String): XML.Elem = super.apply(att, text(txt)) |
|
169 |
def apply(c: String, txt: String): XML.Elem = super.apply(c, text(txt)) |
|
170 |
} |
|
64359 | 171 |
|
172 |
val div = new Operator("div") |
|
173 |
val span = new Operator("span") |
|
65753 | 174 |
val pre = new Operator("pre") |
64359 | 175 |
val par = new Operator("p") |
176 |
val emph = new Operator("em") |
|
177 |
val bold = new Operator("b") |
|
65771 | 178 |
val code = new Operator("code") |
64355 | 179 |
|
64359 | 180 |
val title = new Heading("title") |
181 |
val chapter = new Heading("h1") |
|
182 |
val section = new Heading("h2") |
|
183 |
val subsection = new Heading("h3") |
|
184 |
val subsubsection = new Heading("h4") |
|
185 |
val paragraph = new Heading("h5") |
|
186 |
val subparagraph = new Heading("h6") |
|
187 |
||
188 |
def itemize(items: List[XML.Body]): XML.Elem = |
|
189 |
XML.elem("ul", items.map(XML.elem("li", _))) |
|
190 |
||
191 |
def enumerate(items: List[XML.Body]): XML.Elem = |
|
192 |
XML.elem("ol", items.map(XML.elem("li", _))) |
|
193 |
||
194 |
def description(items: List[(XML.Body, XML.Body)]): XML.Elem = |
|
195 |
XML.elem("dl", items.flatMap({ case (x, y) => List(XML.elem("dt", x), XML.elem("dd", y)) })) |
|
196 |
||
197 |
def link(href: String, body: XML.Body = Nil): XML.Elem = |
|
198 |
XML.Elem(Markup("a", List("href" -> href)), if (body.isEmpty) text(href) else body) |
|
64355 | 199 |
|
65753 | 200 |
def image(src: String, alt: String = ""): XML.Elem = |
201 |
XML.Elem(Markup("img", List("src" -> src) ::: proper_string(alt).map("alt" -> _).toList), Nil) |
|
202 |
||
66040 | 203 |
def source(body: XML.Body): XML.Elem = pre("source", body) |
204 |
def source(src: String): XML.Elem = source(text(src)) |
|
65988 | 205 |
|
65941 | 206 |
def style(s: String): XML.Elem = XML.elem("style", text(s)) |
66000 | 207 |
def style_file(href: String): XML.Elem = |
208 |
XML.Elem(Markup("link", List("rel" -> "stylesheet", "type" -> "text/css", "href" -> href)), Nil) |
|
66212 | 209 |
def style_file(path: Path): XML.Elem = style_file(Url.print_file(path.file)) |
66000 | 210 |
|
66210 | 211 |
def script(s: String): XML.Elem = XML.elem("script", text(s)) |
212 |
def script_file(href: String): XML.Elem = XML.Elem(Markup("script", List("src" -> href)), Nil) |
|
66212 | 213 |
def script_file(path: Path): XML.Elem = script_file(Url.print_file(path.file)) |
214 |
||
37200
0f3edc64356a
added HTML.encode (in Scala), similar to HTML.output in ML;
wenzelm
parents:
36016
diff
changeset
|
215 |
|
65892 | 216 |
/* messages */ |
217 |
||
65939 | 218 |
// background |
65993 | 219 |
val writeln_message: Attribute = class_("writeln_message") |
220 |
val warning_message: Attribute = class_("warning_message") |
|
221 |
val error_message: Attribute = class_("error_message") |
|
65892 | 222 |
|
65939 | 223 |
// underline |
65993 | 224 |
val writeln: Attribute = class_("writeln") |
225 |
val warning: Attribute = class_("warning") |
|
226 |
val error: Attribute = class_("error") |
|
65892 | 227 |
|
65944 | 228 |
|
229 |
/* tooltips */ |
|
230 |
||
231 |
def tooltip(item: XML.Body, tip: XML.Body): XML.Elem = |
|
65992 | 232 |
span(item ::: List(div("tooltip", tip))) |
65944 | 233 |
|
234 |
def tooltip_errors(item: XML.Body, msgs: List[XML.Body]): XML.Elem = |
|
235 |
HTML.error(tooltip(item, msgs.map(msg => error_message(pre(msg))))) |
|
65892 | 236 |
|
237 |
||
66196 | 238 |
/* GUI elements */ |
239 |
||
240 |
object GUI |
|
241 |
{ |
|
242 |
private def optional_value(text: String): XML.Attributes = |
|
243 |
proper_string(text).map(a => "value" -> a).toList |
|
244 |
||
245 |
private def optional_name(name: String): XML.Attributes = |
|
246 |
proper_string(name).map(a => "name" -> a).toList |
|
247 |
||
248 |
private def optional_title(tooltip: String): XML.Attributes = |
|
249 |
proper_string(tooltip).map(a => "title" -> a).toList |
|
250 |
||
251 |
private def optional_submit(submit: Boolean): XML.Attributes = |
|
252 |
if (submit) List("onChange" -> "this.form.submit()") else Nil |
|
253 |
||
254 |
private def optional_checked(selected: Boolean): XML.Attributes = |
|
255 |
if (selected) List("checked" -> "") else Nil |
|
256 |
||
257 |
private def optional_action(action: String): XML.Attributes = |
|
258 |
proper_string(action).map(a => "action" -> a).toList |
|
259 |
||
66210 | 260 |
private def optional_onclick(script: String): XML.Attributes = |
261 |
proper_string(script).map(a => "onclick" -> a).toList |
|
262 |
||
263 |
private def optional_onchange(script: String): XML.Attributes = |
|
264 |
proper_string(script).map(a => "onchange" -> a).toList |
|
265 |
||
266 |
def button(body: XML.Body, name: String = "", tooltip: String = "", submit: Boolean = false, |
|
267 |
script: String = ""): XML.Elem = |
|
66196 | 268 |
XML.Elem( |
269 |
Markup("button", |
|
270 |
List("type" -> (if (submit) "submit" else "button"), "value" -> "true") ::: |
|
66210 | 271 |
optional_name(name) ::: optional_title(tooltip) ::: optional_onclick(script)), body) |
66196 | 272 |
|
273 |
def checkbox(body: XML.Body, name: String = "", tooltip: String = "", submit: Boolean = false, |
|
66210 | 274 |
selected: Boolean = false, script: String = ""): XML.Elem = |
66196 | 275 |
XML.elem("label", |
276 |
XML.elem( |
|
277 |
Markup("input", |
|
278 |
List("type" -> "checkbox", "value" -> "true") ::: optional_name(name) ::: |
|
279 |
optional_title(tooltip) ::: optional_submit(submit) ::: |
|
66210 | 280 |
optional_checked(selected) ::: optional_onchange(script))) :: body) |
66196 | 281 |
|
282 |
def text_field(columns: Int = 0, text: String = "", name: String = "", tooltip: String = "", |
|
66210 | 283 |
submit: Boolean = false, script: String = ""): XML.Elem = |
66196 | 284 |
XML.elem(Markup("input", |
285 |
List("type" -> "text") ::: |
|
286 |
(if (columns > 0) List("size" -> columns.toString) else Nil) ::: |
|
66210 | 287 |
optional_value(text) ::: optional_name(name) ::: optional_title(tooltip) ::: |
288 |
optional_submit(submit) ::: optional_onchange(script))) |
|
66196 | 289 |
|
290 |
def parameter(text: String = "", name: String = ""): XML.Elem = |
|
291 |
XML.elem( |
|
292 |
Markup("input", List("type" -> "hidden") ::: optional_value(text) ::: optional_name(name))) |
|
293 |
||
66209 | 294 |
def form(body: XML.Body, name: String = "", action: String = "", http_post: Boolean = false) |
295 |
: XML.Elem = |
|
296 |
XML.Elem( |
|
297 |
Markup("form", optional_name(name) ::: optional_action(action) ::: |
|
298 |
(if (http_post) List("method" -> "post") else Nil)), body) |
|
66196 | 299 |
} |
300 |
||
301 |
||
66200 | 302 |
/* GUI layout */ |
303 |
||
304 |
object Wrap_Panel |
|
305 |
{ |
|
306 |
object Alignment extends Enumeration |
|
307 |
{ |
|
308 |
val left, right, center = Value |
|
309 |
} |
|
310 |
||
311 |
def apply(contents: List[XML.Elem], name: String = "", action: String = "", |
|
66206 | 312 |
alignment: Alignment.Value = Alignment.right): XML.Elem = |
66200 | 313 |
{ |
314 |
val body = Library.separate(XML.Text(" "), contents) |
|
315 |
GUI.form(List(div(body) + ("style" -> ("text-align: " + alignment))), |
|
316 |
name = name, action = action) |
|
317 |
} |
|
318 |
} |
|
319 |
||
320 |
||
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
50707
diff
changeset
|
321 |
/* document */ |
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
50707
diff
changeset
|
322 |
|
64359 | 323 |
val header: String = |
324 |
"""<?xml version="1.0" encoding="utf-8" ?> |
|
325 |
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd"> |
|
326 |
<html xmlns="http://www.w3.org/1999/xhtml">""" |
|
327 |
||
328 |
val head_meta: XML.Elem = |
|
329 |
XML.Elem(Markup("meta", |
|
330 |
List("http-equiv" -> "Content-Type", "content" -> "text/html; charset=utf-8")), Nil) |
|
331 |
||
65997
e3dc9ea67a62
output control symbols like ML version, with optionally hidden source;
wenzelm
parents:
65993
diff
changeset
|
332 |
def output_document(head: XML.Body, body: XML.Body, |
e3dc9ea67a62
output control symbols like ML version, with optionally hidden source;
wenzelm
parents:
65993
diff
changeset
|
333 |
css: String = "isabelle.css", hidden: Boolean = true): String = |
e3dc9ea67a62
output control symbols like ML version, with optionally hidden source;
wenzelm
parents:
65993
diff
changeset
|
334 |
{ |
64359 | 335 |
cat_lines( |
336 |
List(header, |
|
65997
e3dc9ea67a62
output control symbols like ML version, with optionally hidden source;
wenzelm
parents:
65993
diff
changeset
|
337 |
output( |
66000 | 338 |
XML.elem("head", head_meta :: (if (css == "") Nil else List(style_file(css))) ::: head), |
65997
e3dc9ea67a62
output control symbols like ML version, with optionally hidden source;
wenzelm
parents:
65993
diff
changeset
|
339 |
hidden = hidden), |
e3dc9ea67a62
output control symbols like ML version, with optionally hidden source;
wenzelm
parents:
65993
diff
changeset
|
340 |
output(XML.elem("body", body), hidden = hidden))) |
e3dc9ea67a62
output control symbols like ML version, with optionally hidden source;
wenzelm
parents:
65993
diff
changeset
|
341 |
} |
64359 | 342 |
|
65838 | 343 |
|
66000 | 344 |
/* fonts */ |
345 |
||
346 |
def fonts_url(): String => String = |
|
347 |
(for (font <- Isabelle_System.fonts(html = true)) |
|
348 |
yield (font.base_name -> Url.print_file(font.file))).toMap |
|
349 |
||
350 |
def fonts_dir(prefix: String)(ttf_name: String): String = |
|
351 |
prefix + "/" + ttf_name |
|
352 |
||
353 |
def fonts_css(make_url: String => String = fonts_url()): String = |
|
354 |
{ |
|
355 |
def font_face(name: String, ttf_name: String, bold: Boolean = false): String = |
|
356 |
cat_lines( |
|
357 |
List( |
|
358 |
"@font-face {", |
|
359 |
" font-family: '" + name + "';", |
|
360 |
" src: url('" + make_url(ttf_name) + "') format('truetype');") ::: |
|
361 |
(if (bold) List(" font-weight: bold;") else Nil) ::: |
|
362 |
List("}")) |
|
363 |
||
364 |
List( |
|
365 |
"/* Isabelle fonts */", |
|
366 |
font_face("IsabelleText", "IsabelleText.ttf"), |
|
367 |
font_face("IsabelleText", "IsabelleTextBold.ttf", bold = true), |
|
368 |
font_face("Vacuous", "Vacuous.ttf")).mkString("\n\n") |
|
369 |
} |
|
370 |
||
371 |
||
65838 | 372 |
/* document directory */ |
373 |
||
65998 | 374 |
def isabelle_css: Path = Path.explode("~~/etc/isabelle.css") |
375 |
||
66000 | 376 |
def write_isabelle_css(dir: Path, make_url: String => String = fonts_dir("fonts")) |
377 |
{ |
|
378 |
File.write(dir + isabelle_css.base, |
|
379 |
fonts_css(make_url) + "\n\n\n" + File.read(isabelle_css)) |
|
380 |
} |
|
381 |
||
65836 | 382 |
def init_dir(dir: Path) |
383 |
{ |
|
384 |
Isabelle_System.mkdirs(dir) |
|
66000 | 385 |
write_isabelle_css(dir) |
65836 | 386 |
} |
387 |
||
65838 | 388 |
def write_document(dir: Path, name: String, head: XML.Body, body: XML.Body, |
65999 | 389 |
css: String = isabelle_css.base_name, hidden: Boolean = true) |
65838 | 390 |
{ |
391 |
init_dir(dir) |
|
65997
e3dc9ea67a62
output control symbols like ML version, with optionally hidden source;
wenzelm
parents:
65993
diff
changeset
|
392 |
File.write(dir + Path.basic(name), output_document(head, body, css = css, hidden = hidden)) |
65838 | 393 |
} |
33984 | 394 |
} |