1.1 --- a/src/Tools/jEdit/src/jedit/html_panel.scala	Thu May 20 11:44:41 2010 +0200
     1.2 +++ b/src/Tools/jEdit/src/jedit/html_panel.scala	Thu May 20 13:54:31 2010 +0200
     1.3 @@ -46,8 +46,9 @@
     1.4    Logger.getLogger("org.lobobrowser").setLevel(Level.WARNING)
     1.5  
     1.6  
     1.7 -  /* pixel size -- cf. org.lobobrowser.html.style.HtmlValues.getFontSize */
     1.8 +  /* Lobo setup */
     1.9  
    1.10 +  // pixel size -- cf. org.lobobrowser.html.style.HtmlValues.getFontSize
    1.11    val screen_resolution =
    1.12      if (GraphicsEnvironment.isHeadless()) 72
    1.13      else Toolkit.getDefaultToolkit().getScreenResolution()
    1.14 @@ -56,7 +57,29 @@
    1.15    def raw_px(lobo_px: Int): Int = (lobo_px * screen_resolution + 95) / 96
    1.16  
    1.17  
    1.18 -  /* document template */
    1.19 +  private val ucontext = new SimpleUserAgentContext
    1.20 +  private val rcontext = new SimpleHtmlRendererContext(this, ucontext)
    1.21 +  {
    1.22 +    private def handle(event: HTML_Panel.Event): Boolean =
    1.23 +      if (handler != null && handler.isDefinedAt(event)) { handler(event); true }
    1.24 +      else false
    1.25 +
    1.26 +    override def onContextMenu(elem: HTMLElement, event: MouseEvent): Boolean =
    1.27 +      handle(HTML_Panel.Context_Menu(elem, event))
    1.28 +    override def onMouseClick(elem: HTMLElement, event: MouseEvent): Boolean =
    1.29 +      handle(HTML_Panel.Mouse_Click(elem, event))
    1.30 +    override def onDoubleClick(elem: HTMLElement, event: MouseEvent): Boolean =
    1.31 +      handle(HTML_Panel.Double_Click(elem, event))
    1.32 +    override def onMouseOver(elem: HTMLElement, event: MouseEvent)
    1.33 +      { handle(HTML_Panel.Mouse_Over(elem, event)) }
    1.34 +    override def onMouseOut(elem: HTMLElement, event: MouseEvent)
    1.35 +      { handle(HTML_Panel.Mouse_Out(elem, event)) }
    1.36 +  }
    1.37 +
    1.38 +  private val builder = new DocumentBuilderImpl(ucontext, rcontext)
    1.39 +
    1.40 +
    1.41 +  /* physical document */
    1.42  
    1.43    private def template(font_size: Int): String =
    1.44    {
    1.45 @@ -78,87 +101,66 @@
    1.46  """
    1.47    }
    1.48  
    1.49 -  private def font_metrics(font_size: Int): FontMetrics =
    1.50 -    Swing_Thread.now { getFontMetrics(system.get_font(font_size)) }
    1.51 +  private class Doc
    1.52 +  {
    1.53 +    var current_font_size: Int = 0
    1.54 +    var current_font_metrics: FontMetrics = null
    1.55 +    var current_margin: Int = 0
    1.56 +    var current_body: List[XML.Tree] = Nil
    1.57 +    var current_DOM: org.w3c.dom.Document = null
    1.58  
    1.59 -  private def panel_width(font_size: Int): Int =
    1.60 -    Swing_Thread.now {
    1.61 -      (getWidth() / (font_metrics(font_size).charWidth(Symbol.spc) max 1) - 4) max 20
    1.62 +    def resize(font_size: Int)
    1.63 +    {
    1.64 +      if (font_size != current_font_size || current_font_metrics == null) {
    1.65 +        Swing_Thread.now {
    1.66 +          current_font_size = font_size
    1.67 +          current_font_metrics =
    1.68 +            getFontMetrics(system.get_font(lobo_px(raw_px(font_size))))
    1.69 +          current_margin =
    1.70 +            (getWidth() / (current_font_metrics.charWidth(Symbol.spc) max 1) - 4) max 20
    1.71 +        }
    1.72 +        current_DOM =
    1.73 +          builder.parse(
    1.74 +            new InputSourceImpl(new StringReader(template(font_size)), "http://localhost"))
    1.75 +        render(current_body)
    1.76 +      }
    1.77      }
    1.78  
    1.79 +    def render(body: List[XML.Tree])
    1.80 +    {
    1.81 +      current_body = body
    1.82 +      val html_body =
    1.83 +        current_body.flatMap(div =>
    1.84 +          Pretty.formatted(List(div), current_margin,
    1.85 +              Pretty.font_metric(current_font_metrics))
    1.86 +            .map(t => XML.elem(HTML.PRE, HTML.spans(t))))
    1.87  
    1.88 -  /* actor with local state */
    1.89 +      val node = XML.document_node(current_DOM, XML.elem(HTML.BODY, html_body))
    1.90 +      current_DOM.removeChild(current_DOM.getLastChild())
    1.91 +      current_DOM.appendChild(node)
    1.92 +      Swing_Thread.now { setDocument(current_DOM, rcontext) }
    1.93 +    }
    1.94  
    1.95 -  private val ucontext = new SimpleUserAgentContext
    1.96 -
    1.97 -  private val rcontext = new SimpleHtmlRendererContext(this, ucontext)
    1.98 -  {
    1.99 -    private def handle(event: HTML_Panel.Event): Boolean =
   1.100 -      if (handler != null && handler.isDefinedAt(event)) { handler(event); true }
   1.101 -      else false
   1.102 -
   1.103 -    override def onContextMenu(elem: HTMLElement, event: MouseEvent): Boolean =
   1.104 -      handle(HTML_Panel.Context_Menu(elem, event))
   1.105 -    override def onMouseClick(elem: HTMLElement, event: MouseEvent): Boolean =
   1.106 -      handle(HTML_Panel.Mouse_Click(elem, event))
   1.107 -    override def onDoubleClick(elem: HTMLElement, event: MouseEvent): Boolean =
   1.108 -      handle(HTML_Panel.Double_Click(elem, event))
   1.109 -    override def onMouseOver(elem: HTMLElement, event: MouseEvent)
   1.110 -      { handle(HTML_Panel.Mouse_Over(elem, event)) }
   1.111 -    override def onMouseOut(elem: HTMLElement, event: MouseEvent)
   1.112 -      { handle(HTML_Panel.Mouse_Out(elem, event)) }
   1.113 +    resize(initial_font_size)
   1.114    }
   1.115  
   1.116 -  private val builder = new DocumentBuilderImpl(ucontext, rcontext)
   1.117  
   1.118 -  private case class Init(font_size: Int)
   1.119 -  private case class Render(divs: List[XML.Tree])
   1.120 +  /* main actor and method wrappers */
   1.121 +
   1.122 +  private case class Resize(font_size: Int)
   1.123 +  private case class Render(body: List[XML.Tree])
   1.124  
   1.125    private val main_actor = actor {
   1.126 -    // crude double buffering
   1.127 -    var doc1: org.w3c.dom.Document = null
   1.128 -    var doc2: org.w3c.dom.Document = null
   1.129 -
   1.130 -    var current_font_size = 16
   1.131 -    var current_font_metrics: FontMetrics = null
   1.132 -
   1.133 +    var doc = new Doc
   1.134      loop {
   1.135        react {
   1.136 -        case Init(font_size) =>
   1.137 -          current_font_size = font_size
   1.138 -          current_font_metrics = font_metrics(lobo_px(raw_px(font_size)))
   1.139 -
   1.140 -          val src = template(font_size)
   1.141 -          def parse() =
   1.142 -            builder.parse(new InputSourceImpl(new StringReader(src), "http://localhost"))
   1.143 -          doc1 = parse()
   1.144 -          doc2 = parse()
   1.145 -          Swing_Thread.now { setDocument(doc1, rcontext) }
   1.146 -
   1.147 -        case Render(divs) =>
   1.148 -          val doc = doc2
   1.149 -          val html_body =
   1.150 -            divs.flatMap(div =>
   1.151 -              Pretty.formatted(List(div), panel_width(current_font_size),
   1.152 -                  Pretty.font_metric(current_font_metrics))
   1.153 -                .map(t => XML.elem(HTML.PRE, HTML.spans(t))))
   1.154 -          val node = XML.document_node(doc, XML.elem(HTML.BODY, html_body))
   1.155 -          doc.removeChild(doc.getLastChild())
   1.156 -          doc.appendChild(node)
   1.157 -          doc2 = doc1
   1.158 -          doc1 = doc
   1.159 -          Swing_Thread.now { setDocument(doc1, rcontext) }
   1.160 -
   1.161 +        case Resize(font_size) => doc.resize(font_size)
   1.162 +        case Render(body) => doc.render(body)
   1.163          case bad => System.err.println("main_actor: ignoring bad message " + bad)
   1.164        }
   1.165      }
   1.166    }
   1.167  
   1.168 -
   1.169 -  /* main method wrappers */
   1.170 -
   1.171 -  def init(font_size: Int) { main_actor ! Init(font_size) }
   1.172 -  def render(divs: List[XML.Tree]) { main_actor ! Render(divs) }
   1.173 -
   1.174 -  init(initial_font_size)
   1.175 +  def resize(font_size: Int) { main_actor ! Resize(font_size) }
   1.176 +  def render(body: List[XML.Tree]) { main_actor ! Render(body) }
   1.177  }

     2.1 --- a/src/Tools/jEdit/src/jedit/output_dockable.scala	Thu May 20 11:44:41 2010 +0200
     2.2 +++ b/src/Tools/jEdit/src/jedit/output_dockable.scala	Thu May 20 13:54:31 2010 +0200
     2.3 @@ -67,7 +67,7 @@
     2.4    private val output_actor = actor {
     2.5      loop {
     2.6        react {
     2.7 -        case Session.Global_Settings => html_panel.init(Isabelle.font_size())
     2.8 +        case Session.Global_Settings => html_panel.resize(Isabelle.font_size())
     2.9  
    2.10          case Render(body) => html_panel.render(body)
    2.11