# HG changeset patch
# User wenzelm
# Date 1376392706 -7200
# Node ID 39da27fc6101dc0509a24378bc3ebd312ced81b1
# Parent  9dd1a6dcebfd9a7ffe90c88f8aaa058848efd78f
attempt to transfer focus back to main window after closing popups, which is potentially relevant for heavy-weight windows (cf. workaround in org/gjt/sp/jedit/gui/CompletionPopup.java);

diff -r 9dd1a6dcebfd -r 39da27fc6101 src/Tools/jEdit/src/jedit_lib.scala
--- a/src/Tools/jEdit/src/jedit_lib.scala	Tue Aug 13 12:48:06 2013 +0200
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Tue Aug 13 13:18:26 2013 +0200
@@ -76,6 +76,21 @@
   def buffer_name(buffer: Buffer): String = buffer.getSymlinkPath
 
 
+  /* focus of main window */
+
+  def request_focus_view: Unit =
+  {
+    jEdit.getActiveView() match {
+      case null =>
+      case view =>
+        view.getTextArea match {
+          case null =>
+          case text_area => text_area.requestFocus
+        }
+    }
+  }
+
+
   /* main jEdit components */
 
   def jedit_buffers(): Iterator[Buffer] = jEdit.getBuffers().iterator
diff -r 9dd1a6dcebfd -r 39da27fc6101 src/Tools/jEdit/src/pretty_tooltip.scala
--- a/src/Tools/jEdit/src/pretty_tooltip.scala	Tue Aug 13 12:48:06 2013 +0200
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Tue Aug 13 13:18:26 2013 +0200
@@ -116,7 +116,7 @@
         stack = rest
         rest match {
           case top :: _ => top.request_focus
-          case Nil =>
+          case Nil => JEdit_Lib.request_focus_view
         }
       case _ =>
     }
@@ -129,6 +129,7 @@
     else {
       stack.foreach(_.hide_popup)
       stack = Nil
+      JEdit_Lib.request_focus_view
       true
     }
   }