# HG changeset patch
# User wenzelm
# Date 1504272070 -7200
# Node ID cc93f86e005fde8a6a617a62069fa4ef4d8052f3
# Parent  6efa351190d089c07fa8fda7c645c910943ddbaa
tuned signature;

diff -r 6efa351190d0 -r cc93f86e005f src/Tools/jEdit/src/jedit_lib.scala
--- a/src/Tools/jEdit/src/jedit_lib.scala	Fri Sep 01 15:15:29 2017 +0200
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Fri Sep 01 15:21:10 2017 +0200
@@ -340,6 +340,11 @@
 
   /* key event handling */
 
+  def request_focus_view(alt_view: View = null)
+  {
+    isabelle.jedit_base.JEdit_Lib.request_focus_view(alt_view)
+  }
+
   def propagate_key(view: View, evt: KeyEvent)
   {
     if (view != null && !evt.isConsumed)
diff -r 6efa351190d0 -r cc93f86e005f src/Tools/jEdit/src/pretty_tooltip.scala
--- a/src/Tools/jEdit/src/pretty_tooltip.scala	Fri Sep 01 15:15:29 2017 +0200
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Fri Sep 01 15:21:10 2017 +0200
@@ -136,7 +136,7 @@
       case Some((old, _ :: rest)) =>
         rest match {
           case top :: _ => top.request_focus
-          case Nil => isabelle.jedit_base.JEdit_Lib.request_focus_view()
+          case Nil => JEdit_Lib.request_focus_view()
         }
         old.foreach(_.hide_popup)
         tip.hide_popup
@@ -153,7 +153,7 @@
     deactivate()
     if (stack.isEmpty) false
     else {
-      isabelle.jedit_base.JEdit_Lib.request_focus_view()
+      JEdit_Lib.request_focus_view()
       stack.foreach(_.hide_popup)
       stack = Nil
       true