diff -r 6389a8c1268a -r 42b5d216dc8c src/Tools/jEdit/src/pretty_tooltip.scala
--- a/src/Tools/jEdit/src/pretty_tooltip.scala	Thu May 08 21:17:23 2014 +0200
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Fri May 09 21:02:15 2014 +0200
@@ -136,7 +136,7 @@
       case Some((old, _ :: rest)) =>
         rest match {
           case top :: _ => top.request_focus
-          case Nil => JEdit_Lib.request_focus_view
+          case Nil => JEdit_Lib.request_focus_view()
         }
         old.foreach(_.hide_popup)
         tip.hide_popup
@@ -153,7 +153,7 @@
     deactivate()
     if (stack.isEmpty) false
     else {
-      JEdit_Lib.request_focus_view
+      JEdit_Lib.request_focus_view()
       stack.foreach(_.hide_popup)
       stack = Nil
       true