src/Tools/jEdit/src-base/jedit_lib.scala
author wenzelm
Fri, 01 Sep 2017 15:15:29 +0200
changeset 66591 6efa351190d0
child 73340 0ffcad1f6130
permissions -rw-r--r--
more robust: provide docking framework via base plugin;

/*  Title:      Tools/jEdit/src-base/jedit_lib.scala
    Author:     Makarius

Misc library functions for jEdit.
*/

package isabelle.jedit_base


import isabelle._

import org.gjt.sp.jedit.{jEdit, View}


object JEdit_Lib
{
  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
    }
  }
}