author | wenzelm |
Sat, 27 May 2017 00:30:48 +0200 | |
changeset 65941 | 316c30b60ebc |
parent 65939 | 9fb044904a4d |
child 65942 | 864a4892e43c |
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 |
{ |
|
59063 | 12 |
/* encode text with control symbols */ |
13 |
||
62104
fb73c0d7bb37
clarified symbol insertion, depending on buffer encoding;
wenzelm
parents:
60215
diff
changeset
|
14 |
val control = |
fb73c0d7bb37
clarified symbol insertion, depending on buffer encoding;
wenzelm
parents:
60215
diff
changeset
|
15 |
Map( |
fb73c0d7bb37
clarified symbol insertion, depending on buffer encoding;
wenzelm
parents:
60215
diff
changeset
|
16 |
Symbol.sub -> "sub", |
fb73c0d7bb37
clarified symbol insertion, depending on buffer encoding;
wenzelm
parents:
60215
diff
changeset
|
17 |
Symbol.sub_decoded -> "sub", |
fb73c0d7bb37
clarified symbol insertion, depending on buffer encoding;
wenzelm
parents:
60215
diff
changeset
|
18 |
Symbol.sup -> "sup", |
59063 | 19 |
Symbol.sup_decoded -> "sup", |
62104
fb73c0d7bb37
clarified symbol insertion, depending on buffer encoding;
wenzelm
parents:
60215
diff
changeset
|
20 |
Symbol.bold -> "b", |
59063 | 21 |
Symbol.bold_decoded -> "b") |
37200
0f3edc64356a
added HTML.encode (in Scala), similar to HTML.output in ML;
wenzelm
parents:
36016
diff
changeset
|
22 |
|
64355 | 23 |
def output(text: String, s: StringBuilder) |
37200
0f3edc64356a
added HTML.encode (in Scala), similar to HTML.output in ML;
wenzelm
parents:
36016
diff
changeset
|
24 |
{ |
62113 | 25 |
def output_char(c: Char) = |
59063 | 26 |
c match { |
64355 | 27 |
case '<' => s ++= "<" |
28 |
case '>' => s ++= ">" |
|
29 |
case '&' => s ++= "&" |
|
30 |
case '"' => s ++= """ |
|
31 |
case '\'' => s ++= "'" |
|
32 |
case '\n' => s ++= "<br/>" |
|
33 |
case _ => s += c |
|
59063 | 34 |
} |
64355 | 35 |
def output_chars(str: String) = str.iterator.foreach(output_char(_)) |
59063 | 36 |
|
62104
fb73c0d7bb37
clarified symbol insertion, depending on buffer encoding;
wenzelm
parents:
60215
diff
changeset
|
37 |
var ctrl = "" |
59063 | 38 |
for (sym <- Symbol.iterator(text)) { |
62104
fb73c0d7bb37
clarified symbol insertion, depending on buffer encoding;
wenzelm
parents:
60215
diff
changeset
|
39 |
if (control.isDefinedAt(sym)) ctrl = sym |
59063 | 40 |
else { |
62104
fb73c0d7bb37
clarified symbol insertion, depending on buffer encoding;
wenzelm
parents:
60215
diff
changeset
|
41 |
control.get(ctrl) match { |
59063 | 42 |
case Some(elem) if Symbol.is_controllable(sym) && sym != "\"" => |
64355 | 43 |
s ++= ("<" + elem + ">") |
62113 | 44 |
output_chars(sym) |
64355 | 45 |
s ++= ("</" + elem + ">") |
59063 | 46 |
case _ => |
62113 | 47 |
output_chars(ctrl) |
48 |
output_chars(sym) |
|
59063 | 49 |
} |
62104
fb73c0d7bb37
clarified symbol insertion, depending on buffer encoding;
wenzelm
parents:
60215
diff
changeset
|
50 |
ctrl = "" |
59063 | 51 |
} |
37200
0f3edc64356a
added HTML.encode (in Scala), similar to HTML.output in ML;
wenzelm
parents:
36016
diff
changeset
|
52 |
} |
62113 | 53 |
output_chars(ctrl) |
64355 | 54 |
} |
59063 | 55 |
|
64355 | 56 |
def output(text: String): String = Library.make_string(output(text, _)) |
57 |
||
58 |
||
59 |
/* output XML as HTML */ |
|
60 |
||
65834
67a6e0f166c2
extra space only for some structual elements, but not <a>, <b>, <em> etc. (amending 8a0fe5469ba0);
wenzelm
parents:
65773
diff
changeset
|
61 |
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
|
62 |
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
|
63 |
"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
|
64 |
|
64355 | 65 |
def output(body: XML.Body, s: StringBuilder) |
66 |
{ |
|
67 |
def attrib(p: (String, String)): Unit = |
|
68 |
{ s ++= " "; s ++= p._1; s ++= "=\""; output(p._2, s); s ++= "\"" } |
|
69 |
def elem(markup: Markup): Unit = |
|
70 |
{ s ++= markup.name; markup.properties.foreach(attrib) } |
|
71 |
def tree(t: XML.Tree): Unit = |
|
72 |
t match { |
|
73 |
case XML.Elem(markup, Nil) => |
|
74 |
s ++= "<"; elem(markup); s ++= "/>" |
|
75 |
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
|
76 |
if (structural_elements(markup.name)) s += '\n' |
67a6e0f166c2
extra space only for some structual elements, but not <a>, <b>, <em> etc. (amending 8a0fe5469ba0);
wenzelm
parents:
65773
diff
changeset
|
77 |
s ++= "<"; elem(markup); s ++= ">" |
64355 | 78 |
ts.foreach(tree) |
65834
67a6e0f166c2
extra space only for some structual elements, but not <a>, <b>, <em> etc. (amending 8a0fe5469ba0);
wenzelm
parents:
65773
diff
changeset
|
79 |
s ++= "</"; s ++= markup.name; s ++= ">" |
67a6e0f166c2
extra space only for some structual elements, but not <a>, <b>, <em> etc. (amending 8a0fe5469ba0);
wenzelm
parents:
65773
diff
changeset
|
80 |
if (structural_elements(markup.name)) s += '\n' |
64355 | 81 |
case XML.Text(txt) => output(txt, s) |
82 |
} |
|
83 |
body.foreach(tree) |
|
37200
0f3edc64356a
added HTML.encode (in Scala), similar to HTML.output in ML;
wenzelm
parents:
36016
diff
changeset
|
84 |
} |
0f3edc64356a
added HTML.encode (in Scala), similar to HTML.output in ML;
wenzelm
parents:
36016
diff
changeset
|
85 |
|
64355 | 86 |
def output(body: XML.Body): String = Library.make_string(output(body, _)) |
87 |
def output(tree: XML.Tree): String = output(List(tree)) |
|
88 |
||
89 |
||
65753 | 90 |
/* attributes */ |
91 |
||
65773 | 92 |
def id(s: String): XML.Attribute = ("id" -> s) |
93 |
def width(w: Int): XML.Attribute = ("width" -> w.toString) |
|
94 |
def height(h: Int): XML.Attribute = ("height" -> h.toString) |
|
65892 | 95 |
def css_class(name: String): XML.Attribute = ("class" -> name) |
65753 | 96 |
|
97 |
||
64359 | 98 |
/* structured markup operators */ |
99 |
||
100 |
def text(txt: String): XML.Body = if (txt.isEmpty) Nil else List(XML.Text(txt)) |
|
65753 | 101 |
val break: XML.Body = List(XML.elem("br")) |
64359 | 102 |
|
103 |
class Operator(name: String) |
|
104 |
{ def apply(body: XML.Body): XML.Elem = XML.elem(name, body) } |
|
64356 | 105 |
|
64359 | 106 |
class Heading(name: String) extends Operator(name) |
107 |
{ def apply(txt: String): XML.Elem = super.apply(text(txt)) } |
|
108 |
||
109 |
val div = new Operator("div") |
|
110 |
val span = new Operator("span") |
|
65753 | 111 |
val pre = new Operator("pre") |
64359 | 112 |
val par = new Operator("p") |
113 |
val emph = new Operator("em") |
|
114 |
val bold = new Operator("b") |
|
65771 | 115 |
val code = new Operator("code") |
64355 | 116 |
|
64359 | 117 |
val title = new Heading("title") |
118 |
val chapter = new Heading("h1") |
|
119 |
val section = new Heading("h2") |
|
120 |
val subsection = new Heading("h3") |
|
121 |
val subsubsection = new Heading("h4") |
|
122 |
val paragraph = new Heading("h5") |
|
123 |
val subparagraph = new Heading("h6") |
|
124 |
||
125 |
def itemize(items: List[XML.Body]): XML.Elem = |
|
126 |
XML.elem("ul", items.map(XML.elem("li", _))) |
|
127 |
||
128 |
def enumerate(items: List[XML.Body]): XML.Elem = |
|
129 |
XML.elem("ol", items.map(XML.elem("li", _))) |
|
130 |
||
131 |
def description(items: List[(XML.Body, XML.Body)]): XML.Elem = |
|
132 |
XML.elem("dl", items.flatMap({ case (x, y) => List(XML.elem("dt", x), XML.elem("dd", y)) })) |
|
133 |
||
134 |
def link(href: String, body: XML.Body = Nil): XML.Elem = |
|
135 |
XML.Elem(Markup("a", List("href" -> href)), if (body.isEmpty) text(href) else body) |
|
64355 | 136 |
|
65753 | 137 |
def image(src: String, alt: String = ""): XML.Elem = |
138 |
XML.Elem(Markup("img", List("src" -> src) ::: proper_string(alt).map("alt" -> _).toList), Nil) |
|
139 |
||
65941 | 140 |
def style(s: String): XML.Elem = XML.elem("style", text(s)) |
141 |
||
37200
0f3edc64356a
added HTML.encode (in Scala), similar to HTML.output in ML;
wenzelm
parents:
36016
diff
changeset
|
142 |
|
65892 | 143 |
/* messages */ |
144 |
||
65939 | 145 |
// background |
65892 | 146 |
val writeln_message_class: XML.Attribute = css_class("writeln_message") |
147 |
val warning_message_class: XML.Attribute = css_class("warning_message") |
|
148 |
val error_message_class: XML.Attribute = css_class("error_message") |
|
149 |
||
65939 | 150 |
// underline |
151 |
val writeln_class: XML.Attribute = css_class("writeln") |
|
152 |
val warning_class: XML.Attribute = css_class("warning") |
|
153 |
val error_class: XML.Attribute = css_class("error") |
|
65892 | 154 |
|
65939 | 155 |
// tooltips |
156 |
val tooltip_class: XML.Attribute = css_class("tooltip") |
|
65892 | 157 |
|
158 |
||
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
50707
diff
changeset
|
159 |
/* document */ |
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
50707
diff
changeset
|
160 |
|
64359 | 161 |
val header: String = |
162 |
"""<?xml version="1.0" encoding="utf-8" ?> |
|
163 |
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd"> |
|
164 |
<html xmlns="http://www.w3.org/1999/xhtml">""" |
|
165 |
||
166 |
val head_meta: XML.Elem = |
|
167 |
XML.Elem(Markup("meta", |
|
168 |
List("http-equiv" -> "Content-Type", "content" -> "text/html; charset=utf-8")), Nil) |
|
169 |
||
65836 | 170 |
def head_css(css: String): XML.Elem = |
171 |
XML.Elem(Markup("link", List("rel" -> "stylesheet", "type" -> "text/css", "href" -> css)), Nil) |
|
172 |
||
173 |
def output_document(head: XML.Body, body: XML.Body, css: String = "isabelle.css"): String = |
|
64359 | 174 |
cat_lines( |
175 |
List(header, |
|
65836 | 176 |
output(XML.elem("head", head_meta :: (if (css == "") Nil else List(head_css(css))) ::: head)), |
64359 | 177 |
output(XML.elem("body", body)))) |
178 |
||
65838 | 179 |
|
180 |
/* document directory */ |
|
181 |
||
65836 | 182 |
def init_dir(dir: Path) |
183 |
{ |
|
184 |
Isabelle_System.mkdirs(dir) |
|
185 |
File.copy(Path.explode("~~/etc/isabelle.css"), dir) |
|
186 |
} |
|
187 |
||
65838 | 188 |
def write_document(dir: Path, name: String, head: XML.Body, body: XML.Body, |
189 |
css: String = "isabelle.css") |
|
190 |
{ |
|
191 |
init_dir(dir) |
|
192 |
File.write(dir + Path.basic(name), output_document(head, body, css)) |
|
193 |
} |
|
194 |
||
64359 | 195 |
|
196 |
/* Isabelle document */ |
|
197 |
||
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
50707
diff
changeset
|
198 |
def begin_document(title: String): String = |
64359 | 199 |
header + "\n" + |
200 |
"<head>\n" + output(head_meta) + "\n" + |
|
62113 | 201 |
"<title>" + output(title + " (" + Distribution.version + ")") + "</title>\n" + |
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
50707
diff
changeset
|
202 |
"<link media=\"all\" rel=\"stylesheet\" type=\"text/css\" href=\"isabelle.css\"/>\n" + |
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
50707
diff
changeset
|
203 |
"</head>\n" + |
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
50707
diff
changeset
|
204 |
"\n" + |
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
50707
diff
changeset
|
205 |
"<body>\n" + |
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
50707
diff
changeset
|
206 |
"<div class=\"head\">" + |
62113 | 207 |
"<h1>" + output(title) + "</h1>\n" |
208 |
||
209 |
val end_document = "\n</div>\n</body>\n</html>\n" |
|
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
50707
diff
changeset
|
210 |
|
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
50707
diff
changeset
|
211 |
|
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
50707
diff
changeset
|
212 |
/* common markup elements */ |
33984 | 213 |
|
51402 | 214 |
private def session_entry(entry: (String, String)): String = |
215 |
{ |
|
216 |
val (name, description) = entry |
|
65753 | 217 |
val descr = if (description == "") Nil else break ::: List(pre(text(description))) |
50707
5b2bf7611662
maintain session index on Scala side, for more determistic results;
wenzelm
parents:
50201
diff
changeset
|
218 |
XML.string_of_tree( |
5b2bf7611662
maintain session index on Scala side, for more determistic results;
wenzelm
parents:
50201
diff
changeset
|
219 |
XML.elem("li", |
5b2bf7611662
maintain session index on Scala side, for more determistic results;
wenzelm
parents:
50201
diff
changeset
|
220 |
List(XML.Elem(Markup("a", List(("href", name + "/index.html"))), |
51402 | 221 |
List(XML.Text(name)))) ::: descr)) + "\n" |
222 |
} |
|
34002 | 223 |
|
51402 | 224 |
def chapter_index(chapter: String, sessions: List[(String, String)]): String = |
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
50707
diff
changeset
|
225 |
{ |
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
50707
diff
changeset
|
226 |
begin_document("Isabelle/" + chapter + " sessions") + |
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
50707
diff
changeset
|
227 |
(if (sessions.isEmpty) "" |
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
50707
diff
changeset
|
228 |
else "<div class=\"sessions\"><ul>\n" + sessions.map(session_entry(_)).mkString + "</ul>") + |
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
50707
diff
changeset
|
229 |
end_document |
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
50707
diff
changeset
|
230 |
} |
33984 | 231 |
} |