| changeset 53246 | 8d34caf5bf82 |
| parent 53244 | ec6011bf2362 |
| child 53272 | 0dfd78ff7696 |
| 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 |