# 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) }