tuned signature;

--- a/src/Tools/jEdit/src/jedit_lib.scala	Thu May 08 21:17:23 2014 +0200
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Fri May 09 21:02:15 2014 +0200
@@ -326,9 +326,9 @@
 
   /* key event handling */
 
-  def request_focus_view
+  def request_focus_view(alt_view: View = null)
   {
-    val view = jEdit.getActiveView()
+    val view = if (alt_view != null) alt_view else jEdit.getActiveView()
     if (view != null) {
       val text_area = view.getTextArea
       if (text_area != null) text_area.requestFocus

--- 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