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