# HG changeset patch
# User wenzelm
# Date 1437162315 -7200
# Node ID 7694aa52ad56f0f83774894ba11e6992900de3a9
# Parent  f727b99faaf7c18972be001fdc86439f282988b7
more uniform ComponentAdapter;

diff -r f727b99faaf7 -r 7694aa52ad56 src/Tools/jEdit/src/debugger_dockable.scala
--- a/src/Tools/jEdit/src/debugger_dockable.scala	Fri Jul 17 21:40:47 2015 +0200
+++ b/src/Tools/jEdit/src/debugger_dockable.scala	Fri Jul 17 21:45:15 2015 +0200
@@ -92,6 +92,7 @@
 
   addComponentListener(new ComponentAdapter {
     override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
+    override def componentShown(e: ComponentEvent) { delay_resize.invoke() }
   })
 
 
diff -r f727b99faaf7 -r 7694aa52ad56 src/Tools/jEdit/src/info_dockable.scala
--- a/src/Tools/jEdit/src/info_dockable.scala	Fri Jul 17 21:40:47 2015 +0200
+++ b/src/Tools/jEdit/src/info_dockable.scala	Fri Jul 17 21:45:15 2015 +0200
@@ -86,6 +86,7 @@
 
   addComponentListener(new ComponentAdapter {
     override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
+    override def componentShown(e: ComponentEvent) { delay_resize.invoke() }
   })
 
   private val controls = new Wrap_Panel(Wrap_Panel.Alignment.Right)(
diff -r f727b99faaf7 -r 7694aa52ad56 src/Tools/jEdit/src/output_dockable.scala
--- a/src/Tools/jEdit/src/output_dockable.scala	Fri Jul 17 21:40:47 2015 +0200
+++ b/src/Tools/jEdit/src/output_dockable.scala	Fri Jul 17 21:45:15 2015 +0200
@@ -122,6 +122,7 @@
 
   addComponentListener(new ComponentAdapter {
     override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
+    override def componentShown(e: ComponentEvent) { delay_resize.invoke() }
   })
 
 
diff -r f727b99faaf7 -r 7694aa52ad56 src/Tools/jEdit/src/query_dockable.scala
--- a/src/Tools/jEdit/src/query_dockable.scala	Fri Jul 17 21:40:47 2015 +0200
+++ b/src/Tools/jEdit/src/query_dockable.scala	Fri Jul 17 21:45:15 2015 +0200
@@ -319,6 +319,7 @@
 
   addComponentListener(new ComponentAdapter {
     override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
+    override def componentShown(e: ComponentEvent) { delay_resize.invoke() }
   })
 
 
diff -r f727b99faaf7 -r 7694aa52ad56 src/Tools/jEdit/src/sledgehammer_dockable.scala
--- a/src/Tools/jEdit/src/sledgehammer_dockable.scala	Fri Jul 17 21:40:47 2015 +0200
+++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala	Fri Jul 17 21:45:15 2015 +0200
@@ -66,6 +66,7 @@
 
   addComponentListener(new ComponentAdapter {
     override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
+    override def componentShown(e: ComponentEvent) { delay_resize.invoke() }
   })