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)