equal
deleted
inserted
replaced
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 |