src/Tools/jEdit/src-base/jedit_lib.scala
author wenzelm
Wed, 19 May 2021 11:48:35 +0200
changeset 73739 3e44f8c3f059
parent 73367 77ef8bef0593
permissions -rw-r--r--
default document_build (lualatex);

/*  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): Unit =
  {
    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()
    }
  }
}