# HG changeset patch
# User wenzelm
# Date 1363602590 -3600
# Node ID 14e6d761ba1c1caf8f11bce3cfb31758ea8b89c4
# Parent  e4203ebfe750900c4aefc2757cfb9118c7b9e695
extra tooltip_delay after window.dismiss operation, to avoid flickering of quick reactivation;

diff -r e4203ebfe750 -r 14e6d761ba1c src/Tools/jEdit/etc/options
--- a/src/Tools/jEdit/etc/options	Mon Mar 18 11:04:59 2013 +0100
+++ b/src/Tools/jEdit/etc/options	Mon Mar 18 11:29:50 2013 +0100
@@ -7,7 +7,7 @@
   -- "scale factor of add-on panels wrt. main text area"
 
 option jedit_tooltip_delay : real = 0.75
-  -- "delay for semantic tooltip popup"
+  -- "open/close delay for document tooltips"
 
 option jedit_tooltip_font_scale : real = 0.85
   -- "scale factor of tooltips wrt. main text area"
diff -r e4203ebfe750 -r 14e6d761ba1c src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Mon Mar 18 11:04:59 2013 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Mon Mar 18 11:29:50 2013 +0100
@@ -170,7 +170,7 @@
           Registers.copy(text_area, '$')
           evt.consume
         case KeyEvent.VK_ESCAPE =>
-          Pretty_Tooltip.windows().foreach(_.dispose)
+          Pretty_Tooltip.windows().foreach(_.dismiss)
           evt.consume
         case _ =>
       }
diff -r e4203ebfe750 -r 14e6d761ba1c src/Tools/jEdit/src/pretty_tooltip.scala
--- a/src/Tools/jEdit/src/pretty_tooltip.scala	Mon Mar 18 11:04:59 2013 +0100
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Mon Mar 18 11:29:50 2013 +0100
@@ -63,6 +63,29 @@
     window.init(rendering, mouse_x, mouse_y, results, body)
     window
   }
+
+
+  /* global dismissed delay -- owned by Swing thread */
+
+  private var active = true
+
+  private lazy val reactivate_delay =
+    Swing_Thread.delay_last(PIDE.options.seconds("jedit_tooltip_delay")) {
+      active = true
+    }
+
+  def dismissed
+  {
+    Swing_Thread.require()
+    active = false
+    reactivate_delay.invoke()
+  }
+
+  def is_active: Boolean =
+  {
+    Swing_Thread.require()
+    active
+  }
 }
 
 
@@ -92,7 +115,7 @@
   window.addWindowFocusListener(new WindowAdapter {
     override def windowLostFocus(e: WindowEvent) {
       if (!descendants().exists(_.isDisplayable))
-        window.dispose()
+        window.dismiss
     }
   })
 
@@ -106,7 +129,7 @@
     new JPanel(new BorderLayout) { override def getFocusTraversalKeysEnabled = false }
   window.setContentPane(content_panel)
 
-  val pretty_text_area = new Pretty_Text_Area(view, () => window.dispose(), true) {
+  val pretty_text_area = new Pretty_Text_Area(view, () => window.dismiss, true) {
     override def get_background() = Some(current_rendering.tooltip_color)
   }
   window.add(pretty_text_area)
@@ -118,7 +141,7 @@
     icon = Rendering.tooltip_close_icon
     tooltip = "Close tooltip window"
     listenTo(mouse.clicks)
-    reactions += { case _: MouseClicked => window.dispose() }
+    reactions += { case _: MouseClicked => window.dismiss }
   }
 
   private val detach = new Label {
@@ -128,7 +151,7 @@
     reactions += {
       case _: MouseClicked =>
         Info_Dockable(view, current_rendering.snapshot, current_results, current_body)
-        window.dispose()
+        window.dismiss
     }
   }
 
@@ -136,7 +159,7 @@
   window.add(controls.peer, BorderLayout.NORTH)
 
 
-  /* refresh */
+  /* init */
 
   def init(
     rendering: Rendering,
@@ -202,5 +225,15 @@
     pretty_text_area.requestFocus
     pretty_text_area.refresh()
   }
+
+
+  /* dismiss */
+
+  def dismiss
+  {
+    Swing_Thread.require()
+    Pretty_Tooltip.dismissed
+    window.dispose
+  }
 }
 
diff -r e4203ebfe750 -r 14e6d761ba1c src/Tools/jEdit/src/rich_text_area.scala
--- a/src/Tools/jEdit/src/rich_text_area.scala	Mon Mar 18 11:04:59 2013 +0100
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Mon Mar 18 11:29:50 2013 +0100
@@ -190,8 +190,10 @@
         }
         else active_reset()
 
-        tooltip_event = Some(e)
-        tooltip_delay.invoke()
+        if (Pretty_Tooltip.is_active) {
+          tooltip_event = Some(e)
+          tooltip_delay.invoke()
+        }
       }
     }
   }