isabelle: src/Tools/jEdit/src-base/jedit_lib.scala@3e44f8c3f059 (annotated)

66591 6efa351190d0 more robust: provide docking framework via base plugin; wenzelm parents: diff changeset	1	/* Title: Tools/jEdit/src-base/jedit_lib.scala
6efa351190d0 more robust: provide docking framework via base plugin; wenzelm parents: diff changeset	2	Author: Makarius
6efa351190d0 more robust: provide docking framework via base plugin; wenzelm parents: diff changeset	3
6efa351190d0 more robust: provide docking framework via base plugin; wenzelm parents: diff changeset	4	Misc library functions for jEdit.
6efa351190d0 more robust: provide docking framework via base plugin; wenzelm parents: diff changeset	5	*/
6efa351190d0 more robust: provide docking framework via base plugin; wenzelm parents: diff changeset	6
6efa351190d0 more robust: provide docking framework via base plugin; wenzelm parents: diff changeset	7	package isabelle.jedit_base
6efa351190d0 more robust: provide docking framework via base plugin; wenzelm parents: diff changeset	8
6efa351190d0 more robust: provide docking framework via base plugin; wenzelm parents: diff changeset	9
6efa351190d0 more robust: provide docking framework via base plugin; wenzelm parents: diff changeset	10	import isabelle._
6efa351190d0 more robust: provide docking framework via base plugin; wenzelm parents: diff changeset	11
6efa351190d0 more robust: provide docking framework via base plugin; wenzelm parents: diff changeset	12	import org.gjt.sp.jedit.{jEdit, View}
6efa351190d0 more robust: provide docking framework via base plugin; wenzelm parents: diff changeset	13
6efa351190d0 more robust: provide docking framework via base plugin; wenzelm parents: diff changeset	14
6efa351190d0 more robust: provide docking framework via base plugin; wenzelm parents: diff changeset	15	object JEdit_Lib
6efa351190d0 more robust: provide docking framework via base plugin; wenzelm parents: diff changeset	16	{
73340 0ffcad1f6130 tuned --- fewer warnings; wenzelm parents: 66591 diff changeset	17	def request_focus_view(alt_view: View = null): Unit =
66591 6efa351190d0 more robust: provide docking framework via base plugin; wenzelm parents: diff changeset	18	{
6efa351190d0 more robust: provide docking framework via base plugin; wenzelm parents: diff changeset	19	val view = if (alt_view != null) alt_view else jEdit.getActiveView()
6efa351190d0 more robust: provide docking framework via base plugin; wenzelm parents: diff changeset	20	if (view != null) {
6efa351190d0 more robust: provide docking framework via base plugin; wenzelm parents: diff changeset	21	val text_area = view.getTextArea
73367 77ef8bef0593 clarified signature --- fewer warnings; wenzelm parents: 73340 diff changeset	22	if (text_area != null) text_area.requestFocus()
66591 6efa351190d0 more robust: provide docking framework via base plugin; wenzelm parents: diff changeset	23	}
6efa351190d0 more robust: provide docking framework via base plugin; wenzelm parents: diff changeset	24	}
6efa351190d0 more robust: provide docking framework via base plugin; wenzelm parents: diff changeset	25	}

author	wenzelm
	Wed, 19 May 2021 11:48:35 +0200
changeset 73739	3e44f8c3f059
parent 73367	77ef8bef0593
permissions	-rw-r--r--