reduced cluttering of popups;

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