src/Tools/jEdit/src/output_dockable.scala
changeset 49195 9d10bd85c1be
parent 49071 c1ca931b3647
child 49288 2c9272cb4568
--- a/src/Tools/jEdit/src/output_dockable.scala	Fri Sep 07 13:58:43 2012 +0200
+++ b/src/Tools/jEdit/src/output_dockable.scala	Fri Sep 07 13:58:54 2012 +0200
@@ -141,7 +141,7 @@
     Isabelle.session.global_settings -= main_actor
     Isabelle.session.commands_changed -= main_actor
     Isabelle.session.caret_focus -= main_actor
-    delay_resize(false)
+    delay_resize.revoke()
   }
 
 
@@ -151,7 +151,7 @@
     Swing_Thread.delay_first(Isabelle.session.update_delay) { handle_resize() }
 
   addComponentListener(new ComponentAdapter {
-    override def componentResized(e: ComponentEvent) { delay_resize(true) }
+    override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
   })