328 val header: String = |
328 val header: String = |
329 XML.header + |
329 XML.header + |
330 """<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd"> |
330 """<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd"> |
331 <html xmlns="http://www.w3.org/1999/xhtml">""" |
331 <html xmlns="http://www.w3.org/1999/xhtml">""" |
332 |
332 |
|
333 val footer: String = """</html>""" |
|
334 |
333 val head_meta: XML.Elem = |
335 val head_meta: XML.Elem = |
334 XML.Elem(Markup("meta", |
336 XML.Elem(Markup("meta", |
335 List("http-equiv" -> "Content-Type", "content" -> "text/html; charset=utf-8")), Nil) |
337 List("http-equiv" -> "Content-Type", "content" -> "text/html; charset=utf-8")), Nil) |
336 |
338 |
337 def output_document(head: XML.Body, body: XML.Body, |
339 def output_document(head: XML.Body, body: XML.Body, |
338 css: String = "isabelle.css", |
340 css: String = "isabelle.css", |
339 hidden: Boolean = true, |
341 hidden: Boolean = true, |
340 structural: Boolean = true): String = |
342 structural: Boolean = true): String = |
341 { |
343 { |
342 cat_lines( |
344 cat_lines( |
343 List(header, |
345 List( |
|
346 header, |
344 output( |
347 output( |
345 XML.elem("head", head_meta :: (if (css == "") Nil else List(style_file(css))) ::: head), |
348 XML.elem("head", head_meta :: (if (css == "") Nil else List(style_file(css))) ::: head), |
346 hidden = hidden, structural = structural), |
349 hidden = hidden, structural = structural), |
347 output(XML.elem("body", body), |
350 output(XML.elem("body", body), |
348 hidden = hidden, structural = structural))) |
351 hidden = hidden, structural = structural), |
|
352 footer)) |
349 } |
353 } |
350 |
354 |
351 |
355 |
352 /* fonts */ |
356 /* fonts */ |
353 |
357 |