| author | wenzelm |
| Wed, 19 May 2021 11:48:35 +0200 | |
| changeset 73739 | 3e44f8c3f059 |
| parent 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() } } }