src/Tools/jEdit/src/plugin.scala
changeset 53246 8d34caf5bf82
parent 53244 ec6011bf2362
child 53272 0dfd78ff7696
equal deleted inserted replaced
53245:301b69957af7 53246:8d34caf5bf82
    55 
    55 
    56   /* popups */
    56   /* popups */
    57 
    57 
    58   def dismissed_popups(view: View): Boolean =
    58   def dismissed_popups(view: View): Boolean =
    59   {
    59   {
    60     val b1 = Completion_Popup.dismissed_view(view)
    60     val b1 = Completion_Popup.dismissed(view.getLayeredPane)
    61     val b2 = Pretty_Tooltip.dismissed_all()
    61     val b2 = Pretty_Tooltip.dismissed_all()
    62     b1 || b2
    62     b1 || b2
    63   }
    63   }
    64 
    64 
    65 
    65