# HG changeset patch
# User wenzelm
# Date 1274381786 -7200
# Node ID 1af0f718ffdcf138f629ddd057e7c2ce2554edad
# Parent  641923374eba0b6f8a2c23d2536c2c8146524952
handle component resize for output / HTML panel;

diff -r 641923374eba -r 1af0f718ffdc src/Tools/jEdit/src/jedit/html_panel.scala
--- a/src/Tools/jEdit/src/jedit/html_panel.scala	Thu May 20 20:22:00 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/html_panel.scala	Thu May 20 20:56:26 2010 +0200
@@ -103,10 +103,10 @@
 
   private class Doc
   {
-    var current_font_size: Int = 0
-    var current_font_metrics: FontMetrics = null
-    var current_body: List[XML.Tree] = Nil
-    var current_DOM: org.w3c.dom.Document = null
+    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
 
     def resize(font_size: Int)
     {
@@ -119,10 +119,12 @@
         current_DOM =
           builder.parse(
             new InputSourceImpl(new StringReader(template(font_size)), "http://localhost"))
-        render(current_body)
+        refresh()
       }
     }
 
+    def refresh() { render(current_body) }
+
     def render(body: List[XML.Tree])
     {
       current_body = body
@@ -147,12 +149,14 @@
 
   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 bad => System.err.println("main_actor: ignoring bad message " + bad)
       }
@@ -160,5 +164,6 @@
   }
 
   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) }
 }
diff -r 641923374eba -r 1af0f718ffdc src/Tools/jEdit/src/jedit/output_dockable.scala
--- a/src/Tools/jEdit/src/jedit/output_dockable.scala	Thu May 20 20:22:00 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/output_dockable.scala	Thu May 20 20:56:26 2010 +0200
@@ -16,6 +16,7 @@
 
 import javax.swing.JPanel
 import java.awt.{BorderLayout, Dimension}
+import java.awt.event.{ComponentEvent, ComponentAdapter}
 
 import org.gjt.sp.jedit.View
 import org.gjt.sp.jedit.gui.DockableWindowManager
@@ -68,7 +69,6 @@
     loop {
       react {
         case Session.Global_Settings => html_panel.resize(Isabelle.font_size())
-
         case Render(body) => html_panel.render(body)
 
         case cmd: Command =>
@@ -99,6 +99,14 @@
   }
 
 
+  /* resize */
+
+  addComponentListener(new ComponentAdapter {
+    val delay = Swing_Thread.delay_last(500) { html_panel.refresh() }
+    override def componentResized(e: ComponentEvent) { delay() }
+  })
+
+
   /* init controls */
 
   controls.contents ++= List(update, follow)