src/Tools/jEdit/src/jedit_lib.scala
changeset 56930 42b5d216dc8c
parent 56823 37be55461dbe
child 57612 990ffb84489b
     1.1 --- a/src/Tools/jEdit/src/jedit_lib.scala	Thu May 08 21:17:23 2014 +0200
     1.2 +++ b/src/Tools/jEdit/src/jedit_lib.scala	Fri May 09 21:02:15 2014 +0200
     1.3 @@ -326,9 +326,9 @@
     1.4  
     1.5    /* key event handling */
     1.6  
     1.7 -  def request_focus_view
     1.8 +  def request_focus_view(alt_view: View = null)
     1.9    {
    1.10 -    val view = jEdit.getActiveView()
    1.11 +    val view = if (alt_view != null) alt_view else jEdit.getActiveView()
    1.12      if (view != null) {
    1.13        val text_area = view.getTextArea
    1.14        if (text_area != null) text_area.requestFocus