# HG changeset patch
# User wenzelm
# Date 1399662135 -7200
# Node ID 42b5d216dc8cc2b3b5071fb1235cdddbb0f86a8e
# Parent  6389a8c1268a82ec803d4f33304126e3a24455b9
tuned signature;

diff -r 6389a8c1268a -r 42b5d216dc8c src/Tools/jEdit/src/jedit_lib.scala
--- 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
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