1/* Title: Tools/jEdit/src-base/jedit_lib.scala 2 Author: Makarius 3 4Misc library functions for jEdit. 5*/ 6 7package isabelle.jedit_base 8 9 10import isabelle._ 11 12import org.gjt.sp.jedit.{jEdit, View} 13 14 15object JEdit_Lib 16{ 17 def request_focus_view(alt_view: View = null) 18 { 19 val view = if (alt_view != null) alt_view else jEdit.getActiveView() 20 if (view != null) { 21 val text_area = view.getTextArea 22 if (text_area != null) text_area.requestFocus 23 } 24 } 25}