7 package isabelle |
7 package isabelle |
8 |
8 |
9 |
9 |
10 object HTML |
10 object HTML |
11 { |
11 { |
12 /* encode text with control symbols */ |
12 /* output text with control symbols */ |
13 |
13 |
14 val control = |
14 private val control = |
15 Map( |
15 Map( |
16 Symbol.sub -> "sub", |
16 Symbol.sub -> "sub", Symbol.sub_decoded -> "sub", |
17 Symbol.sub_decoded -> "sub", |
17 Symbol.sup -> "sup", Symbol.sup_decoded -> "sup", |
18 Symbol.sup -> "sup", |
18 Symbol.bold -> "b", Symbol.bold_decoded -> "b") |
19 Symbol.sup_decoded -> "sup", |
19 |
20 Symbol.bold -> "b", |
20 private val control_block = |
21 Symbol.bold_decoded -> "b") |
21 Map( |
22 |
22 Symbol.bsub -> "<sub>", Symbol.bsub_decoded -> "<sub>", |
23 def output(text: String, s: StringBuilder) |
23 Symbol.esub -> "</sub>", Symbol.esub_decoded -> "</sub>", |
24 { |
24 Symbol.bsup -> "<sup>", Symbol.bsup_decoded -> "<sup>", |
25 def output_string(str: String) = XML.output_string(str, s) |
25 Symbol.esup -> "</sup>", Symbol.esup_decoded -> "</sup>") |
|
26 |
|
27 def is_control(sym: Symbol.Symbol): Boolean = control.isDefinedAt(sym) |
|
28 |
|
29 def output(text: String, s: StringBuilder, hidden: Boolean) |
|
30 { |
|
31 def output_hidden(body: => Unit): Unit = |
|
32 if (hidden) { s ++= "<span class=\"hidden\">"; body; s ++= "</span>" } |
|
33 |
|
34 def output_symbol(sym: Symbol.Symbol): Unit = |
|
35 if (sym != "") { |
|
36 control_block.get(sym) match { |
|
37 case Some(html) if html.startsWith("</") => |
|
38 s ++= html; output_hidden(XML.output_string(sym, s)) |
|
39 case Some(html) => |
|
40 output_hidden(XML.output_string(sym, s)); s ++= html |
|
41 case None => |
|
42 XML.output_string(sym, s) |
|
43 } |
|
44 } |
26 |
45 |
27 var ctrl = "" |
46 var ctrl = "" |
28 for (sym <- Symbol.iterator(text)) { |
47 for (sym <- Symbol.iterator(text)) { |
29 if (control.isDefinedAt(sym)) ctrl = sym |
48 if (is_control(sym)) { output_symbol(ctrl); ctrl = sym } |
30 else { |
49 else { |
31 control.get(ctrl) match { |
50 control.get(ctrl) match { |
32 case Some(elem) if Symbol.is_controllable(sym) && sym != "\"" => |
51 case Some(elem) if Symbol.is_controllable(sym) && sym != "\"" => |
|
52 output_hidden(output_symbol(ctrl)) |
33 s += '<'; s ++= elem; s += '>' |
53 s += '<'; s ++= elem; s += '>' |
34 output_string(sym) |
54 output_symbol(sym) |
35 s ++= "</"; s ++= elem; s += '>' |
55 s ++= "</"; s ++= elem; s += '>' |
36 case _ => |
56 case _ => |
37 output_string(ctrl) |
57 output_symbol(ctrl) |
38 output_string(sym) |
58 output_symbol(sym) |
39 } |
59 } |
40 ctrl = "" |
60 ctrl = "" |
41 } |
61 } |
42 } |
62 } |
43 output_string(ctrl) |
63 output_symbol(ctrl) |
44 } |
64 } |
45 |
65 |
46 def output(text: String): String = Library.make_string(output(text, _)) |
66 def output(text: String): String = Library.make_string(output(text, _, hidden = false)) |
47 |
67 |
48 |
68 |
49 /* output XML as HTML */ |
69 /* output XML as HTML */ |
50 |
70 |
51 private val structural_elements = |
71 private val structural_elements = |
52 Set("head", "body", "meta", "div", "pre", "p", "title", "h1", "h2", "h3", "h4", "h5", "h6", |
72 Set("head", "body", "meta", "div", "pre", "p", "title", "h1", "h2", "h3", "h4", "h5", "h6", |
53 "ul", "ol", "dl", "li", "dt", "dd") |
73 "ul", "ol", "dl", "li", "dt", "dd") |
54 |
74 |
55 def output(body: XML.Body, s: StringBuilder) |
75 def output(body: XML.Body, s: StringBuilder, hidden: Boolean) |
56 { |
76 { |
57 def elem(markup: Markup) |
77 def elem(markup: Markup) |
58 { |
78 { |
59 s ++= markup.name |
79 s ++= markup.name |
60 for ((a, b) <- markup.properties) { |
80 for ((a, b) <- markup.properties) { |
61 s += ' '; s ++= a; s += '='; s += '"'; output(b, s); s += '"' |
81 s += ' '; s ++= a; s += '='; s += '"'; output(b, s, hidden); s += '"' |
62 } |
82 } |
63 } |
83 } |
64 def tree(t: XML.Tree): Unit = |
84 def tree(t: XML.Tree): Unit = |
65 t match { |
85 t match { |
66 case XML.Elem(markup, Nil) => |
86 case XML.Elem(markup, Nil) => |
69 if (structural_elements(markup.name)) s += '\n' |
89 if (structural_elements(markup.name)) s += '\n' |
70 s += '<'; elem(markup); s += '>' |
90 s += '<'; elem(markup); s += '>' |
71 ts.foreach(tree) |
91 ts.foreach(tree) |
72 s ++= "</"; s ++= markup.name; s += '>' |
92 s ++= "</"; s ++= markup.name; s += '>' |
73 if (structural_elements(markup.name)) s += '\n' |
93 if (structural_elements(markup.name)) s += '\n' |
74 case XML.Text(txt) => output(txt, s) |
94 case XML.Text(txt) => |
|
95 output(txt, s, hidden) |
75 } |
96 } |
76 body.foreach(tree) |
97 body.foreach(tree) |
77 } |
98 } |
78 |
99 |
79 def output(body: XML.Body): String = Library.make_string(output(body, _)) |
100 def output(body: XML.Body, hidden: Boolean): String = |
80 def output(tree: XML.Tree): String = output(List(tree)) |
101 Library.make_string(output(body, _, hidden)) |
|
102 |
|
103 def output(tree: XML.Tree, hidden: Boolean): String = |
|
104 output(List(tree), hidden) |
81 |
105 |
82 |
106 |
83 /* attributes */ |
107 /* attributes */ |
84 |
108 |
85 class Attribute(val name: String, value: String) |
109 class Attribute(val name: String, value: String) |
185 List("http-equiv" -> "Content-Type", "content" -> "text/html; charset=utf-8")), Nil) |
209 List("http-equiv" -> "Content-Type", "content" -> "text/html; charset=utf-8")), Nil) |
186 |
210 |
187 def head_css(css: String): XML.Elem = |
211 def head_css(css: String): XML.Elem = |
188 XML.Elem(Markup("link", List("rel" -> "stylesheet", "type" -> "text/css", "href" -> css)), Nil) |
212 XML.Elem(Markup("link", List("rel" -> "stylesheet", "type" -> "text/css", "href" -> css)), Nil) |
189 |
213 |
190 def output_document(head: XML.Body, body: XML.Body, css: String = "isabelle.css"): String = |
214 def output_document(head: XML.Body, body: XML.Body, |
|
215 css: String = "isabelle.css", hidden: Boolean = true): String = |
|
216 { |
191 cat_lines( |
217 cat_lines( |
192 List(header, |
218 List(header, |
193 output(XML.elem("head", head_meta :: (if (css == "") Nil else List(head_css(css))) ::: head)), |
219 output( |
194 output(XML.elem("body", body)))) |
220 XML.elem("head", head_meta :: (if (css == "") Nil else List(head_css(css))) ::: head), |
|
221 hidden = hidden), |
|
222 output(XML.elem("body", body), hidden = hidden))) |
|
223 } |
195 |
224 |
196 |
225 |
197 /* document directory */ |
226 /* document directory */ |
198 |
227 |
199 def init_dir(dir: Path) |
228 def init_dir(dir: Path) |