more uniform ComponentAdapter;

--- 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() }
   })
 
 

--- 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)(

--- 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() }
   })
 
 

--- 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() }
   })
 
 

--- 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() }
   })