transfer focus before closing old component -- avoid intermediate focus switch to root component, which is actually visible e.g. on Windows;
--- a/src/Tools/jEdit/src/completion_popup.scala Thu Nov 07 19:35:57 2013 +0100
+++ b/src/Tools/jEdit/src/completion_popup.scala Fri Nov 08 15:10:16 2013 +0100
@@ -490,9 +490,8 @@
private def hide_popup()
{
- val had_focus = list_view.peer.isFocusOwner
+ if (list_view.peer.isFocusOwner) refocus()
popup.hide
- if (had_focus) refocus()
}
}
--- a/src/Tools/jEdit/src/pretty_tooltip.scala Thu Nov 07 19:35:57 2013 +0100
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala Fri Nov 08 15:10:16 2013 +0100
@@ -115,13 +115,13 @@
deactivate()
hierarchy(tip) match {
case Some((old, _ :: rest)) =>
- old.foreach(_.hide_popup)
- tip.hide_popup
- stack = rest
rest match {
case top :: _ => top.request_focus
case Nil => JEdit_Lib.request_focus_view
}
+ old.foreach(_.hide_popup)
+ tip.hide_popup
+ stack = rest
case _ =>
}
}
@@ -131,9 +131,9 @@
deactivate()
if (stack.isEmpty) false
else {
+ JEdit_Lib.request_focus_view
stack.foreach(_.hide_popup)
stack = Nil
- JEdit_Lib.request_focus_view
true
}
}