more uniform ComponentAdapter;
authorwenzelm
Fri Jul 17 21:45:15 2015 +0200 (2015-07-17)
changeset 607507694aa52ad56
parent 60749 f727b99faaf7
child 60751 83f04804696c
more uniform ComponentAdapter;
src/Tools/jEdit/src/debugger_dockable.scala
src/Tools/jEdit/src/info_dockable.scala
src/Tools/jEdit/src/output_dockable.scala
src/Tools/jEdit/src/query_dockable.scala
src/Tools/jEdit/src/sledgehammer_dockable.scala
     1.1 --- a/src/Tools/jEdit/src/debugger_dockable.scala	Fri Jul 17 21:40:47 2015 +0200
     1.2 +++ b/src/Tools/jEdit/src/debugger_dockable.scala	Fri Jul 17 21:45:15 2015 +0200
     1.3 @@ -92,6 +92,7 @@
     1.4  
     1.5    addComponentListener(new ComponentAdapter {
     1.6      override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
     1.7 +    override def componentShown(e: ComponentEvent) { delay_resize.invoke() }
     1.8    })
     1.9  
    1.10  
     2.1 --- a/src/Tools/jEdit/src/info_dockable.scala	Fri Jul 17 21:40:47 2015 +0200
     2.2 +++ b/src/Tools/jEdit/src/info_dockable.scala	Fri Jul 17 21:45:15 2015 +0200
     2.3 @@ -86,6 +86,7 @@
     2.4  
     2.5    addComponentListener(new ComponentAdapter {
     2.6      override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
     2.7 +    override def componentShown(e: ComponentEvent) { delay_resize.invoke() }
     2.8    })
     2.9  
    2.10    private val controls = new Wrap_Panel(Wrap_Panel.Alignment.Right)(
     3.1 --- a/src/Tools/jEdit/src/output_dockable.scala	Fri Jul 17 21:40:47 2015 +0200
     3.2 +++ b/src/Tools/jEdit/src/output_dockable.scala	Fri Jul 17 21:45:15 2015 +0200
     3.3 @@ -122,6 +122,7 @@
     3.4  
     3.5    addComponentListener(new ComponentAdapter {
     3.6      override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
     3.7 +    override def componentShown(e: ComponentEvent) { delay_resize.invoke() }
     3.8    })
     3.9  
    3.10  
     4.1 --- a/src/Tools/jEdit/src/query_dockable.scala	Fri Jul 17 21:40:47 2015 +0200
     4.2 +++ b/src/Tools/jEdit/src/query_dockable.scala	Fri Jul 17 21:45:15 2015 +0200
     4.3 @@ -319,6 +319,7 @@
     4.4  
     4.5    addComponentListener(new ComponentAdapter {
     4.6      override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
     4.7 +    override def componentShown(e: ComponentEvent) { delay_resize.invoke() }
     4.8    })
     4.9  
    4.10  
     5.1 --- a/src/Tools/jEdit/src/sledgehammer_dockable.scala	Fri Jul 17 21:40:47 2015 +0200
     5.2 +++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala	Fri Jul 17 21:45:15 2015 +0200
     5.3 @@ -66,6 +66,7 @@
     5.4  
     5.5    addComponentListener(new ComponentAdapter {
     5.6      override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
     5.7 +    override def componentShown(e: ComponentEvent) { delay_resize.invoke() }
     5.8    })
     5.9  
    5.10