src/Tools/jEdit/src/plugin.scala
changeset 53272 0dfd78ff7696
parent 53246 8d34caf5bf82
child 53274 1760c01f1c78
equal deleted inserted replaced
53271:0460d6962ced 53272:0dfd78ff7696
    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.getLayeredPane)
    60     var dismissed = false
    61     val b2 = Pretty_Tooltip.dismissed_all()
    61 
    62     b1 || b2
    62     for {
       
    63       text_area <- JEdit_Lib.jedit_text_areas(view)
       
    64       doc_view <- document_view(text_area)
       
    65     } { if (doc_view.dismissed_popups()) dismissed = true }
       
    66 
       
    67     if (Pretty_Tooltip.dismissed_all()) dismissed = true
       
    68 
       
    69     dismissed
    63   }
    70   }
    64 
    71 
    65 
    72 
    66   /* document model and view */
    73   /* document model and view */
    67 
    74