# HG changeset patch
# User wenzelm
# Date 1397053326 -7200
# Node ID 0c63f3538639d3086c5a15c65c0b18c0a8450d19
# Parent  46b29bb1c627974662c61d8b2b6c76634263ca53
dismiss popups more carefully (amending 7e8c11011fdf), notably allow mouse dragging within some tooltip, e.g. for text selection;

diff -r 46b29bb1c627 -r 0c63f3538639 src/Tools/jEdit/src/pretty_tooltip.scala
--- a/src/Tools/jEdit/src/pretty_tooltip.scala	Wed Apr 09 15:19:22 2014 +0200
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Wed Apr 09 16:22:06 2014 +0200
@@ -36,6 +36,9 @@
     else None
   }
 
+  private def descendant(parent: JComponent): Option[Pretty_Tooltip] =
+    Swing_Thread.require { stack.find(tip => tip.original_parent == parent) }
+
   def apply(
     view: View,
     parent: JComponent,
@@ -60,7 +63,7 @@
             old.foreach(_.hide_popup)
 
             val loc = SwingUtilities.convertPoint(parent, location, layered)
-            val tip = new Pretty_Tooltip(view, layered, loc, rendering, results, info)
+            val tip = new Pretty_Tooltip(view, layered, parent, loc, rendering, results, info)
             stack = tip :: rest
             tip.show_popup
         }
@@ -142,6 +145,9 @@
     }
   }
 
+  def dismiss_descendant(parent: JComponent): Unit =
+    descendant(parent).foreach(dismiss(_))
+
   def dismissed_all(): Boolean =
   {
     deactivate()
@@ -159,6 +165,7 @@
 class Pretty_Tooltip private(
   view: View,
   layered: JLayeredPane,
+  val original_parent: JComponent,
   location: Point,
   rendering: Rendering,
   private val results: Command.Results,
diff -r 46b29bb1c627 -r 0c63f3538639 src/Tools/jEdit/src/rich_text_area.scala
--- a/src/Tools/jEdit/src/rich_text_area.scala	Wed Apr 09 15:19:22 2014 +0200
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Wed Apr 09 16:22:06 2014 +0200
@@ -202,7 +202,8 @@
   private val mouse_motion_listener = new MouseMotionAdapter {
     override def mouseDragged(evt: MouseEvent) {
       robust_body(()) {
-        PIDE.dismissed_popups(view)
+        Completion_Popup.Text_Area.dismissed(text_area)
+        Pretty_Tooltip.dismiss_descendant(text_area.getPainter)
       }
     }