changeset 67337 | 4254cfd15b00 |
parent 67336 | 3ee6da378183 |
child 69343 | 395c4fb15ea2 |
67336:3ee6da378183 | 67337:4254cfd15b00 |
---|---|
95 |
95 |
96 private val structural_elements = |
96 private val structural_elements = |
97 Set("head", "body", "meta", "div", "pre", "p", "title", "h1", "h2", "h3", "h4", "h5", "h6", |
97 Set("head", "body", "meta", "div", "pre", "p", "title", "h1", "h2", "h3", "h4", "h5", "h6", |
98 "ul", "ol", "dl", "li", "dt", "dd") |
98 "ul", "ol", "dl", "li", "dt", "dd") |
99 |
99 |
100 def output(body: XML.Body, s: StringBuilder, hidden: Boolean) |
100 def output(body: XML.Body, s: StringBuilder, hidden: Boolean, structural: Boolean) |
101 { |
101 { |
102 def elem(markup: Markup) |
102 def elem(markup: Markup) |
103 { |
103 { |
104 s ++= markup.name |
104 s ++= markup.name |
105 for ((a, b) <- markup.properties) { |
105 for ((a, b) <- markup.properties) { |
114 def tree(t: XML.Tree): Unit = |
114 def tree(t: XML.Tree): Unit = |
115 t match { |
115 t match { |
116 case XML.Elem(markup, Nil) => |
116 case XML.Elem(markup, Nil) => |
117 s += '<'; elem(markup); s ++= "/>" |
117 s += '<'; elem(markup); s ++= "/>" |
118 case XML.Elem(markup, ts) => |
118 case XML.Elem(markup, ts) => |
119 if (structural_elements(markup.name)) s += '\n' |
119 if (structural && structural_elements(markup.name)) s += '\n' |
120 s += '<'; elem(markup); s += '>' |
120 s += '<'; elem(markup); s += '>' |
121 ts.foreach(tree) |
121 ts.foreach(tree) |
122 s ++= "</"; s ++= markup.name; s += '>' |
122 s ++= "</"; s ++= markup.name; s += '>' |
123 if (structural_elements(markup.name)) s += '\n' |
123 if (structural && structural_elements(markup.name)) s += '\n' |
124 case XML.Text(txt) => |
124 case XML.Text(txt) => |
125 output(txt, s, hidden = hidden, permissive = true) |
125 output(txt, s, hidden = hidden, permissive = true) |
126 } |
126 } |
127 body.foreach(tree) |
127 body.foreach(tree) |
128 } |
128 } |
129 |
129 |
130 def output(body: XML.Body, hidden: Boolean): String = |
130 def output(body: XML.Body, hidden: Boolean, structural: Boolean): String = |
131 Library.make_string(output(body, _, hidden)) |
131 Library.make_string(output(body, _, hidden, structural)) |
132 |
132 |
133 def output(tree: XML.Tree, hidden: Boolean): String = |
133 def output(tree: XML.Tree, hidden: Boolean, structural: Boolean): String = |
134 output(List(tree), hidden) |
134 output(List(tree), hidden, structural) |
135 |
135 |
136 |
136 |
137 /* attributes */ |
137 /* attributes */ |
138 |
138 |
139 class Attribute(val name: String, value: String) |
139 class Attribute(val name: String, value: String) |
331 val head_meta: XML.Elem = |
331 val head_meta: XML.Elem = |
332 XML.Elem(Markup("meta", |
332 XML.Elem(Markup("meta", |
333 List("http-equiv" -> "Content-Type", "content" -> "text/html; charset=utf-8")), Nil) |
333 List("http-equiv" -> "Content-Type", "content" -> "text/html; charset=utf-8")), Nil) |
334 |
334 |
335 def output_document(head: XML.Body, body: XML.Body, |
335 def output_document(head: XML.Body, body: XML.Body, |
336 css: String = "isabelle.css", hidden: Boolean = true): String = |
336 css: String = "isabelle.css", |
337 hidden: Boolean = true, |
|
338 structural: Boolean = true): String = |
|
337 { |
339 { |
338 cat_lines( |
340 cat_lines( |
339 List(header, |
341 List(header, |
340 output( |
342 output( |
341 XML.elem("head", head_meta :: (if (css == "") Nil else List(style_file(css))) ::: head), |
343 XML.elem("head", head_meta :: (if (css == "") Nil else List(style_file(css))) ::: head), |
342 hidden = hidden), |
344 hidden = hidden, structural = structural), |
343 output(XML.elem("body", body), hidden = hidden))) |
345 output(XML.elem("body", body), |
346 hidden = hidden, structural = structural))) |
|
344 } |
347 } |
345 |
348 |
346 |
349 |
347 /* fonts */ |
350 /* fonts */ |
348 |
351 |
387 Isabelle_System.mkdirs(dir) |
390 Isabelle_System.mkdirs(dir) |
388 write_isabelle_css(dir) |
391 write_isabelle_css(dir) |
389 } |
392 } |
390 |
393 |
391 def write_document(dir: Path, name: String, head: XML.Body, body: XML.Body, |
394 def write_document(dir: Path, name: String, head: XML.Body, body: XML.Body, |
392 css: String = isabelle_css.base_name, hidden: Boolean = true) |
395 css: String = isabelle_css.base_name, |
396 hidden: Boolean = true, |
|
397 structural: Boolean = true) |
|
393 { |
398 { |
394 init_dir(dir) |
399 init_dir(dir) |
395 File.write(dir + Path.basic(name), output_document(head, body, css = css, hidden = hidden)) |
400 File.write(dir + Path.basic(name), |
401 output_document(head, body, css = css, hidden = hidden, structural = structural)) |
|
396 } |
402 } |
397 } |
403 } |