src/Tools/jEdit/src/jedit_lib.scala

     }
 
 
   /* key event handling */
 
-  def request_focus_view
-  {
-    val view = jEdit.getActiveView()
+  def request_focus_view(alt_view: View = null)
+  {
+    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
     }
   }