author | wenzelm |
Mon, 01 Mar 2021 22:22:12 +0100 | |
changeset 73340 | 0ffcad1f6130 |
parent 66591 | 6efa351190d0 |
child 73367 | 77ef8bef0593 |
permissions | -rw-r--r-- |
/* 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 } } }