1.1 --- a/src/Tools/jEdit/src/jedit/html_panel.scala	Fri May 21 11:12:54 2010 +0200
     1.2 +++ b/src/Tools/jEdit/src/jedit/html_panel.scala	Fri May 21 11:16:01 2010 +0200
     1.3 @@ -42,13 +42,15 @@
     1.4    initial_font_size: Int,
     1.5    handler: PartialFunction[HTML_Panel.Event, Unit]) extends HtmlPanel
     1.6  {
     1.7 -  // global logging
     1.8 +  /** Lobo setup **/
     1.9 +
    1.10 +  /* global logging */
    1.11 +
    1.12    Logger.getLogger("org.lobobrowser").setLevel(Level.WARNING)
    1.13  
    1.14  
    1.15 -  /* Lobo setup */
    1.16 +  /* pixel size -- cf. org.lobobrowser.html.style.HtmlValues.getFontSize */
    1.17  
    1.18 -  // pixel size -- cf. org.lobobrowser.html.style.HtmlValues.getFontSize
    1.19    val screen_resolution =
    1.20      if (GraphicsEnvironment.isHeadless()) 72
    1.21      else Toolkit.getDefaultToolkit().getScreenResolution()
    1.22 @@ -106,26 +108,37 @@
    1.23      template_tail
    1.24  
    1.25  
    1.26 -  /* physical document */
    1.27 +  /** main actor **/
    1.28  
    1.29 -  private class Doc
    1.30 -  {
    1.31 -    private var current_font_size: Int = 0
    1.32 -    private var current_font_metrics: FontMetrics = null
    1.33 -    private var current_body: List[XML.Tree] = Nil
    1.34 -    private var current_DOM: org.w3c.dom.Document = null
    1.35 +  /* internal messages */
    1.36 +
    1.37 +  private case class Resize(font_size: Int)
    1.38 +  private case class Render(body: List[XML.Tree])
    1.39 +  private case object Refresh
    1.40 +
    1.41 +  private val main_actor = actor {
    1.42 +
    1.43 +    /* internal state */
    1.44 +
    1.45 +    var current_font_metrics: FontMetrics = null
    1.46 +    var current_font_size: Int = 0
    1.47 +    var current_margin: Int = 0
    1.48 +    var current_body: List[XML.Tree] = Nil
    1.49  
    1.50      def resize(font_size: Int)
    1.51      {
    1.52 -      if (font_size != current_font_size || current_font_metrics == null) {
    1.53 +      val (font_metrics, margin) =
    1.54          Swing_Thread.now {
    1.55 -          current_font_size = font_size
    1.56 -          current_font_metrics =
    1.57 -            getFontMetrics(system.get_font(lobo_px(raw_px(font_size))))
    1.58 +          val metrics = getFontMetrics(system.get_font(lobo_px(raw_px(font_size))))
    1.59 +          (metrics, (getWidth() / (metrics.charWidth(Symbol.spc) max 1) - 4) max 20)
    1.60          }
    1.61 -        current_DOM =
    1.62 -          builder.parse(
    1.63 -            new InputSourceImpl(new StringReader(template(font_size)), "http://localhost"))
    1.64 +      if (current_font_metrics == null ||
    1.65 +          current_font_size != font_size ||
    1.66 +          current_margin != margin)
    1.67 +      {
    1.68 +        current_font_metrics = font_metrics
    1.69 +        current_font_size = font_size
    1.70 +        current_margin = margin
    1.71          refresh()
    1.72        }
    1.73      }
    1.74 @@ -135,43 +148,36 @@
    1.75      def render(body: List[XML.Tree])
    1.76      {
    1.77        current_body = body
    1.78 -      val margin = (getWidth() / (current_font_metrics.charWidth(Symbol.spc) max 1) - 4) max 20
    1.79        val html_body =
    1.80          current_body.flatMap(div =>
    1.81 -          Pretty.formatted(List(div), margin,
    1.82 -              Pretty.font_metric(current_font_metrics))
    1.83 +          Pretty.formatted(List(div), current_margin, Pretty.font_metric(current_font_metrics))
    1.84              .map(t => XML.elem(HTML.PRE, HTML.spans(t))))
    1.85 -
    1.86 -      val node = XML.document_node(current_DOM, XML.elem(HTML.BODY, html_body))
    1.87 -      Swing_Thread.now {
    1.88 -        current_DOM.removeChild(current_DOM.getLastChild())
    1.89 -        current_DOM.appendChild(node)
    1.90 -        setDocument(current_DOM, rcontext)
    1.91 -      }
    1.92 +      val doc =
    1.93 +        builder.parse(
    1.94 +          new InputSourceImpl(new StringReader(template(current_font_size)), "http://localhost"))
    1.95 +      doc.removeChild(doc.getLastChild())
    1.96 +      doc.appendChild(XML.document_node(doc, XML.elem(HTML.BODY, html_body)))
    1.97 +      Swing_Thread.later { setDocument(doc, rcontext) }
    1.98      }
    1.99  
   1.100 +
   1.101 +    /* main loop */
   1.102 +
   1.103      resize(initial_font_size)
   1.104 -  }
   1.105  
   1.106 -
   1.107 -  /* main actor and method wrappers */
   1.108 -
   1.109 -  private case class Resize(font_size: Int)
   1.110 -  private case class Render(body: List[XML.Tree])
   1.111 -  private case object Refresh
   1.112 -
   1.113 -  private val main_actor = actor {
   1.114 -    var doc = new Doc
   1.115      loop {
   1.116        react {
   1.117 -        case Resize(font_size) => doc.resize(font_size)
   1.118 -        case Refresh => doc.refresh()
   1.119 -        case Render(body) => doc.render(body)
   1.120 +        case Resize(font_size) => resize(font_size)
   1.121 +        case Refresh => refresh()
   1.122 +        case Render(body) => render(body)
   1.123          case bad => System.err.println("main_actor: ignoring bad message " + bad)
   1.124        }
   1.125      }
   1.126    }
   1.127  
   1.128 +
   1.129 +  /* external methods */
   1.130 +
   1.131    def resize(font_size: Int) { main_actor ! Resize(font_size) }
   1.132    def refresh() { main_actor ! Refresh }
   1.133    def render(body: List[XML.Tree]) { main_actor ! Render(body) }