1.1 --- a/src/Tools/jEdit/src/jedit/html_panel.scala Thu May 20 20:56:26 2010 +0200
1.2 +++ b/src/Tools/jEdit/src/jedit/html_panel.scala Thu May 20 21:07:05 2010 +0200
1.3 @@ -79,10 +79,9 @@
1.4 private val builder = new DocumentBuilderImpl(ucontext, rcontext)
1.5
1.6
1.7 - /* physical document */
1.8 + /* document template with style sheets */
1.9
1.10 - private def template(font_size: Int): String =
1.11 - {
1.12 + private val template_head =
1.13 """<?xml version="1.0" encoding="utf-8"?>
1.14 <!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN"
1.15 "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
1.16 @@ -91,15 +90,23 @@
1.17 <style media="all" type="text/css">
1.18 """ +
1.19 system.try_read("$ISABELLE_HOME/lib/html/isabelle.css") + "\n" +
1.20 - system.try_read("$ISABELLE_HOME_USER/etc/isabelle.css") + "\n" +
1.21 - "body { font-family: " + system.font_family + "; font-size: " + raw_px(font_size) + "px }" +
1.22 + system.try_read("$ISABELLE_HOME_USER/etc/isabelle.css") + "\n"
1.23 +
1.24 + private val template_tail =
1.25 """
1.26 </style>
1.27 </head>
1.28 <body/>
1.29 </html>
1.30 """
1.31 - }
1.32 +
1.33 + private def template(font_size: Int): String =
1.34 + template_head +
1.35 + "body { font-family: " + system.font_family + "; font-size: " + raw_px(font_size) + "px }" +
1.36 + template_tail
1.37 +
1.38 +
1.39 + /* physical document */
1.40
1.41 private class Doc
1.42 {