# HG changeset patch
# User wenzelm
# Date 1397650582 -7200
# Node ID 68b7a6db4a3223076f54f4c1b75fa7c34609b307
# Parent  46313aafaf87a7fb42c37fd327e9e27bf6f62b5b
avoid ooddity: invoke intended function instead of java.awt.Container.invalidate();

diff -r 46313aafaf87 -r 68b7a6db4a32 src/Tools/jEdit/src/completion_popup.scala
--- a/src/Tools/jEdit/src/completion_popup.scala	Wed Apr 16 13:48:35 2014 +0200
+++ b/src/Tools/jEdit/src/completion_popup.scala	Wed Apr 16 14:16:22 2014 +0200
@@ -254,7 +254,6 @@
             Font_Info.main_size(PIDE.options.real("jedit_popup_font_scale")))
 
         val range = result.range
-        def invalidate(): Unit = JEdit_Lib.invalidate_range(text_area, range)
 
         val loc1 = text_area.offsetToXY(range.start)
         if (loc1 != null) {
@@ -286,12 +285,12 @@
                 if (view.getKeyEventInterceptor == inner_key_listener)
                   view.setKeyEventInterceptor(null)
                 if (focus) text_area.requestFocus
-                invalidate()
+                JEdit_Lib.invalidate_range(text_area, range)
               }
             }
           completion_popup = Some(completion)
           view.setKeyEventInterceptor(completion.inner_key_listener)
-          invalidate()
+          JEdit_Lib.invalidate_range(text_area, range)
           completion.show_popup(false)
         }
       }