src/Tools/jEdit/src/pretty_tooltip.scala

     deactivate()
     hierarchy(tip) match {
       case Some((old, _ :: rest)) =>
         rest match {
           case top :: _ => top.request_focus
-          case Nil => isabelle.jedit_base.JEdit_Lib.request_focus_view()
+          case Nil => JEdit_Lib.request_focus_view()
         }
         old.foreach(_.hide_popup)
         tip.hide_popup
         stack = rest
       case _ =>

   def dismissed_all(): Boolean =
   {
     deactivate()
     if (stack.isEmpty) false
     else {
-      isabelle.jedit_base.JEdit_Lib.request_focus_view()
+      JEdit_Lib.request_focus_view()
       stack.foreach(_.hide_popup)
       stack = Nil
       true
     }
   }