component resize: full handle_resize;

--- a/src/Tools/jEdit/src/jedit/output_dockable.scala	Thu May 20 21:19:38 2010 -0700
+++ b/src/Tools/jEdit/src/jedit/output_dockable.scala	Fri May 21 11:12:54 2010 +0200
@@ -111,7 +111,7 @@
   /* resize */
 
   addComponentListener(new ComponentAdapter {
-    val delay = Swing_Thread.delay_last(500) { html_panel.refresh() }
+    val delay = Swing_Thread.delay_last(500) { handle_resize() }
     override def componentResized(e: ComponentEvent) { delay() }
   })