equal
deleted
inserted
replaced
134 deactivate() |
134 deactivate() |
135 hierarchy(tip) match { |
135 hierarchy(tip) match { |
136 case Some((old, _ :: rest)) => |
136 case Some((old, _ :: rest)) => |
137 rest match { |
137 rest match { |
138 case top :: _ => top.request_focus |
138 case top :: _ => top.request_focus |
139 case Nil => JEdit_Lib.request_focus_view |
139 case Nil => JEdit_Lib.request_focus_view() |
140 } |
140 } |
141 old.foreach(_.hide_popup) |
141 old.foreach(_.hide_popup) |
142 tip.hide_popup |
142 tip.hide_popup |
143 stack = rest |
143 stack = rest |
144 case _ => |
144 case _ => |
151 def dismissed_all(): Boolean = |
151 def dismissed_all(): Boolean = |
152 { |
152 { |
153 deactivate() |
153 deactivate() |
154 if (stack.isEmpty) false |
154 if (stack.isEmpty) false |
155 else { |
155 else { |
156 JEdit_Lib.request_focus_view |
156 JEdit_Lib.request_focus_view() |
157 stack.foreach(_.hide_popup) |
157 stack.foreach(_.hide_popup) |
158 stack = Nil |
158 stack = Nil |
159 true |
159 true |
160 } |
160 } |
161 } |
161 } |