reduced cluttering of popups;
authorwenzelm
Sat May 03 20:20:55 2014 +0200 (2014-05-03 ago)
changeset 56841bc6faeadbf82
parent 56840 879fe16bd27c
child 56842 b6e266574b26
reduced cluttering of popups;
src/Tools/jEdit/src/completion_popup.scala
     1.1 --- a/src/Tools/jEdit/src/completion_popup.scala	Sat May 03 20:10:49 2014 +0200
     1.2 +++ b/src/Tools/jEdit/src/completion_popup.scala	Sat May 03 20:20:55 2014 +0200
     1.3 @@ -293,6 +293,7 @@
     1.4            completion_popup = Some(completion)
     1.5            view.setKeyEventInterceptor(completion.inner_key_listener)
     1.6            JEdit_Lib.invalidate_range(text_area, range)
     1.7 +          Pretty_Tooltip.dismissed_all()
     1.8            completion.show_popup(false)
     1.9          }
    1.10        }