# HG changeset patch
# User wenzelm
# Date 1375803009 -7200
# Node ID e2d5c3ff5c3f3cd985a0df531b2be7292eb486ca
# Parent  91032244e4caded284e4ac844ff3b96b42cf75ab
tuned signature;

diff -r 91032244e4ca -r e2d5c3ff5c3f src/Tools/jEdit/src/query_operation.scala
--- a/src/Tools/jEdit/src/query_operation.scala	Mon Aug 05 23:57:29 2013 +0200
+++ b/src/Tools/jEdit/src/query_operation.scala	Tue Aug 06 17:30:09 2013 +0200
@@ -34,7 +34,7 @@
   private val instance = Document_ID.make().toString
 
 
-  /* status animation */
+  /* animation */
 
   private val passive_icon =
     JEdit_Lib.load_image_icon(PIDE.options.string("process_passive_icon")).getImage
@@ -43,9 +43,19 @@
       JEdit_Lib.load_image_icon(name).getImage)
 
   val animation = new Label
-  val animation_icon = new AnimatedIcon(passive_icon, active_icons.toArray, 10, animation.peer)
+  private val animation_icon =
+    new AnimatedIcon(passive_icon, active_icons.toArray, 10, animation.peer)
   animation.icon = animation_icon
 
+  private def animation_rate(rate: Int)
+  {
+    animation_icon.stop
+    if (rate > 0) {
+      animation_icon.setRate(rate)
+      animation_icon.start
+    }
+  }
+
 
   /* implicit state -- owned by Swing thread */
 
@@ -96,7 +106,7 @@
 
     if (!new_output.isEmpty) {
       current_result = true
-      animation_icon.stop
+      animation_rate(0)
       remove_overlay()
       PIDE.flush_buffers()
     }
@@ -117,7 +127,7 @@
         current_location = None
         current_query = Nil
         current_result = false
-        animation_icon.start
+        animation_rate(10)
         snapshot.node.command_at(doc_view.text_area.getCaretPosition).map(_._1) match {
           case Some(command) =>
             current_location = Some(command)