src/Tools/jEdit/src/pretty_tooltip.scala
changeset 56930 42b5d216dc8c
parent 56662 f373fb77e0a4
child 57612 990ffb84489b
equal deleted inserted replaced
56919:6389a8c1268a 56930:42b5d216dc8c
   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   }