src/Tools/jEdit/src/jedit_lib.scala
changeset 53003 39da27fc6101
parent 52874 91032244e4ca
child 53019 be9e94594b96
     1.1 --- a/src/Tools/jEdit/src/jedit_lib.scala	Tue Aug 13 12:48:06 2013 +0200
     1.2 +++ b/src/Tools/jEdit/src/jedit_lib.scala	Tue Aug 13 13:18:26 2013 +0200
     1.3 @@ -76,6 +76,21 @@
     1.4    def buffer_name(buffer: Buffer): String = buffer.getSymlinkPath
     1.5  
     1.6  
     1.7 +  /* focus of main window */
     1.8 +
     1.9 +  def request_focus_view: Unit =
    1.10 +  {
    1.11 +    jEdit.getActiveView() match {
    1.12 +      case null =>
    1.13 +      case view =>
    1.14 +        view.getTextArea match {
    1.15 +          case null =>
    1.16 +          case text_area => text_area.requestFocus
    1.17 +        }
    1.18 +    }
    1.19 +  }
    1.20 +
    1.21 +
    1.22    /* main jEdit components */
    1.23  
    1.24    def jedit_buffers(): Iterator[Buffer] = jEdit.getBuffers().iterator