# HG changeset patch # User wenzelm # Date 1274382425 -7200 # Node ID 39207774a9b74f6efb32d9b5aa554da68e304783 # Parent 1af0f718ffdcf138f629ddd057e7c2ce2554edad read style sheets only once; diff -r 1af0f718ffdc -r 39207774a9b7 src/Tools/jEdit/src/jedit/html_panel.scala --- a/src/Tools/jEdit/src/jedit/html_panel.scala Thu May 20 20:56:26 2010 +0200 +++ b/src/Tools/jEdit/src/jedit/html_panel.scala Thu May 20 21:07:05 2010 +0200 @@ -79,10 +79,9 @@ private val builder = new DocumentBuilderImpl(ucontext, rcontext) - /* physical document */ + /* document template with style sheets */ - private def template(font_size: Int): String = - { + private val template_head = """ @@ -91,15 +90,23 @@ """ - } + + private def template(font_size: Int): String = + template_head + + "body { font-family: " + system.font_family + "; font-size: " + raw_px(font_size) + "px }" + + template_tail + + + /* physical document */ private class Doc {