# HG changeset patch
# User wenzelm
# Date 1399141255 -7200
# Node ID bc6faeadbf82e65caa5cb3975fcca2e123756240
# Parent  879fe16bd27c06d9e7f0528f2b19f4a85889043e
reduced cluttering of popups;

diff -r 879fe16bd27c -r bc6faeadbf82 src/Tools/jEdit/src/completion_popup.scala
--- a/src/Tools/jEdit/src/completion_popup.scala	Sat May 03 20:10:49 2014 +0200
+++ b/src/Tools/jEdit/src/completion_popup.scala	Sat May 03 20:20:55 2014 +0200
@@ -293,6 +293,7 @@
           completion_popup = Some(completion)
           view.setKeyEventInterceptor(completion.inner_key_listener)
           JEdit_Lib.invalidate_range(text_area, range)
+          Pretty_Tooltip.dismissed_all()
           completion.show_popup(false)
         }
       }