src/Tools/jEdit/src/completion_popup.scala
changeset 56841 bc6faeadbf82
parent 56840 879fe16bd27c
child 56842 b6e266574b26
equal deleted inserted replaced
56840:879fe16bd27c 56841:bc6faeadbf82
   291               }
   291               }
   292             }
   292             }
   293           completion_popup = Some(completion)
   293           completion_popup = Some(completion)
   294           view.setKeyEventInterceptor(completion.inner_key_listener)
   294           view.setKeyEventInterceptor(completion.inner_key_listener)
   295           JEdit_Lib.invalidate_range(text_area, range)
   295           JEdit_Lib.invalidate_range(text_area, range)
       
   296           Pretty_Tooltip.dismissed_all()
   296           completion.show_popup(false)
   297           completion.show_popup(false)
   297         }
   298         }
   298       }
   299       }
   299 
   300 
   300       if (buffer.isEditable) {
   301       if (buffer.isEditable) {