# HG changeset patch
# User wenzelm
# Date 1373910669 -7200
# Node ID e99a0a43720b1f0303fb1bb4cb63b1c2ddc260ac
# Parent  6e71d43775e56930b37626c23c1c37faafd15c42
deactivate/revoke mouse event more thoroughly, to avoid "Implicit change of text area buffer";

diff -r 6e71d43775e5 -r e99a0a43720b src/Tools/jEdit/src/pretty_tooltip.scala
--- a/src/Tools/jEdit/src/pretty_tooltip.scala	Mon Jul 15 19:23:19 2013 +0200
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Mon Jul 15 19:51:09 2013 +0200
@@ -85,6 +85,12 @@
       }
     }
 
+  def revoke(): Unit =
+    Swing_Thread.required {
+      pending = None
+      pending_delay.revoke()
+    }
+
   private lazy val reactivate_delay =
     Swing_Thread.delay_last(PIDE.options.seconds("jedit_tooltip_delay")) {
       active = true
@@ -92,9 +98,8 @@
 
   private def deactivate(): Unit =
     Swing_Thread.required {
-      pending = None
+      revoke()
       active = false
-      pending_delay.revoke()
       reactivate_delay.invoke()
     }
 
@@ -118,13 +123,15 @@
   }
 
   def dismissed_all(): Boolean =
+  {
+    deactivate()
     if (stack.isEmpty) false
     else {
-      deactivate()
       stack.foreach(_.hide_popup)
       stack = Nil
       true
     }
+  }
 
 
   /* auxiliary geometry measurement */