# HG changeset patch # User wenzelm # Date 1274433361 -7200 # Node ID 9640f654617907e1bc85f6945dd6863a71461802 # Parent 0e4073f19825b34127798b3beb87b1bc7c7caa3d more systematic treatment of internal state, which belongs strictly to the main actor, not the Swing thread; do not re-use mutable DOM -- avoid races wrt. the rendering engine; more thorough resize -- always recalculate metrics/margin synchronously; asynchronous setDocument; tuned; diff -r 0e4073f19825 -r 9640f6546179 src/Tools/jEdit/src/jedit/html_panel.scala --- a/src/Tools/jEdit/src/jedit/html_panel.scala Fri May 21 11:12:54 2010 +0200 +++ b/src/Tools/jEdit/src/jedit/html_panel.scala Fri May 21 11:16:01 2010 +0200 @@ -42,13 +42,15 @@ initial_font_size: Int, handler: PartialFunction[HTML_Panel.Event, Unit]) extends HtmlPanel { - // global logging + /** Lobo setup **/ + + /* global logging */ + Logger.getLogger("org.lobobrowser").setLevel(Level.WARNING) - /* Lobo setup */ + /* pixel size -- cf. org.lobobrowser.html.style.HtmlValues.getFontSize */ - // pixel size -- cf. org.lobobrowser.html.style.HtmlValues.getFontSize val screen_resolution = if (GraphicsEnvironment.isHeadless()) 72 else Toolkit.getDefaultToolkit().getScreenResolution() @@ -106,26 +108,37 @@ template_tail - /* physical document */ + /** main actor **/ + + /* internal messages */ + + private case class Resize(font_size: Int) + private case class Render(body: List[XML.Tree]) + private case object Refresh - private class Doc - { - private var current_font_size: Int = 0 - private var current_font_metrics: FontMetrics = null - private var current_body: List[XML.Tree] = Nil - private var current_DOM: org.w3c.dom.Document = null + private val main_actor = actor { + + /* internal state */ + + var current_font_metrics: FontMetrics = null + var current_font_size: Int = 0 + var current_margin: Int = 0 + var current_body: List[XML.Tree] = Nil def resize(font_size: Int) { - if (font_size != current_font_size || current_font_metrics == null) { + val (font_metrics, margin) = Swing_Thread.now { - current_font_size = font_size - current_font_metrics = - getFontMetrics(system.get_font(lobo_px(raw_px(font_size)))) + val metrics = getFontMetrics(system.get_font(lobo_px(raw_px(font_size)))) + (metrics, (getWidth() / (metrics.charWidth(Symbol.spc) max 1) - 4) max 20) } - current_DOM = - builder.parse( - new InputSourceImpl(new StringReader(template(font_size)), "http://localhost")) + if (current_font_metrics == null || + current_font_size != font_size || + current_margin != margin) + { + current_font_metrics = font_metrics + current_font_size = font_size + current_margin = margin refresh() } } @@ -135,43 +148,36 @@ def render(body: List[XML.Tree]) { current_body = body - val margin = (getWidth() / (current_font_metrics.charWidth(Symbol.spc) max 1) - 4) max 20 val html_body = current_body.flatMap(div => - Pretty.formatted(List(div), margin, - Pretty.font_metric(current_font_metrics)) + Pretty.formatted(List(div), current_margin, Pretty.font_metric(current_font_metrics)) .map(t => XML.elem(HTML.PRE, HTML.spans(t)))) + val doc = + builder.parse( + new InputSourceImpl(new StringReader(template(current_font_size)), "http://localhost")) + doc.removeChild(doc.getLastChild()) + doc.appendChild(XML.document_node(doc, XML.elem(HTML.BODY, html_body))) + Swing_Thread.later { setDocument(doc, rcontext) } + } - val node = XML.document_node(current_DOM, XML.elem(HTML.BODY, html_body)) - Swing_Thread.now { - current_DOM.removeChild(current_DOM.getLastChild()) - current_DOM.appendChild(node) - setDocument(current_DOM, rcontext) - } - } + + /* main loop */ resize(initial_font_size) - } - - /* main actor and method wrappers */ - - private case class Resize(font_size: Int) - private case class Render(body: List[XML.Tree]) - private case object Refresh - - private val main_actor = actor { - var doc = new Doc loop { react { - case Resize(font_size) => doc.resize(font_size) - case Refresh => doc.refresh() - case Render(body) => doc.render(body) + case Resize(font_size) => resize(font_size) + case Refresh => refresh() + case Render(body) => render(body) case bad => System.err.println("main_actor: ignoring bad message " + bad) } } } + + /* external methods */ + def resize(font_size: Int) { main_actor ! Resize(font_size) } def refresh() { main_actor ! Refresh } def render(body: List[XML.Tree]) { main_actor ! Render(body) }