separate Process_Indicator -- simplified/clarified version of org.gjt.sp.jedit.gui.AnimatedIcon;

--- a/src/Tools/jEdit/lib/Tools/jedit	Fri Aug 09 12:29:15 2013 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit	Fri Aug 09 13:37:51 2013 +0200
@@ -34,6 +34,7 @@
   "src/plugin.scala"
   "src/pretty_text_area.scala"
   "src/pretty_tooltip.scala"
+  "src/process_indicator.scala"
   "src/protocol_dockable.scala"
   "src/query_operation.scala"
   "src/raw_output_dockable.scala"

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/process_indicator.scala	Fri Aug 09 13:37:51 2013 +0200
@@ -0,0 +1,65 @@
+/*  Title:      Tools/jEdit/src/process_indicator.scala
+    Author:     Makarius
+
+Process indicator with animated icon.
+*/
+
+package isabelle.jedit
+
+
+import isabelle._
+
+import java.awt.Image
+import java.awt.event.{ActionListener, ActionEvent}
+import javax.swing.{ImageIcon, Timer}
+import scala.swing.{Label, Component}
+
+
+class Process_Indicator
+{
+  private val label = new Label
+
+  private val passive_icon =
+    JEdit_Lib.load_image_icon(PIDE.options.string("process_passive_icon")).getImage
+  private val active_icons =
+    space_explode(':', PIDE.options.string("process_active_icons")).map(name =>
+      JEdit_Lib.load_image_icon(name).getImage)
+
+  private val animation = new ImageIcon(passive_icon) {
+    private var current_frame = 0
+    private val timer =
+      new Timer(0, new ActionListener {
+        override def actionPerformed(e: ActionEvent) {
+          current_frame = (current_frame + 1) % active_icons.length
+          setImage(active_icons(current_frame))
+          label.repaint
+        }
+      })
+    timer.setRepeats(true)
+
+    def update(rate: Int)
+    {
+      if (rate == 0) {
+        setImage(passive_icon)
+        timer.stop
+        label.repaint
+      }
+      else {
+        val delay = 1000 / rate
+        timer.setInitialDelay(delay)
+        timer.setDelay(delay)
+        timer.restart
+      }
+    }
+  }
+  label.icon = animation
+
+  def component: Component = label
+
+  def update(tip: String, rate: Int)
+  {
+    label.tooltip = tip
+    animation.update(rate)
+  }
+}
+

--- a/src/Tools/jEdit/src/query_operation.scala	Fri Aug 09 12:29:15 2013 +0200
+++ b/src/Tools/jEdit/src/query_operation.scala	Fri Aug 09 13:37:51 2013 +0200
@@ -11,10 +11,9 @@
 import isabelle._
 
 import scala.actors.Actor._
-import scala.swing.Label
+import scala.swing.Component
 
 import org.gjt.sp.jedit.View
-import org.gjt.sp.jedit.gui.AnimatedIcon
 
 
 object Query_Operation
@@ -72,34 +71,20 @@
   }
 
 
-  /* animation */
-
-  val animation = new Label
+  /* process indicator */
 
-  private val passive_icon =
-    JEdit_Lib.load_image_icon(PIDE.options.string("process_passive_icon")).getImage
-  private val active_icons =
-    space_explode(':', PIDE.options.string("process_active_icons")).map(name =>
-      JEdit_Lib.load_image_icon(name).getImage)
+  private val process_indicator = new Process_Indicator
+  val animation: Component = process_indicator.component
 
-  private val animation_icon =
-    new AnimatedIcon(passive_icon, active_icons.toArray, 5, animation.peer)
-  animation.icon = animation_icon
-
-  private def animation_update()
+  private def update_process_indicator()
   {
-    animation_icon.stop
     current_status match {
       case Status.WAITING =>
-        animation.tooltip = "Waiting for evaluation of query context ..."
-        animation_icon.setRate(5)
-        animation_icon.start
+        process_indicator.update("Waiting for evaluation of query context ...", 5)
       case Status.RUNNING =>
-        animation.tooltip = "Running query operation ..."
-        animation_icon.setRate(15)
-        animation_icon.start
+        process_indicator.update("Running query operation ...", 15)
       case Status.FINISHED =>
-        animation.tooltip = null
+        process_indicator.update(null, 0)
     }
   }
 
@@ -173,7 +158,7 @@
         }
         if (current_status != new_status) {
           current_status = new_status
-          animation_update()
+          update_process_indicator()
           if (new_status == Status.FINISHED) {
             remove_overlay()
             PIDE.flush_buffers()
@@ -207,7 +192,7 @@
             doc_view.model.insert_overlay(command, operation_name, instance :: query)
           case None =>
         }
-        animation_update()
+        update_process_indicator()
         PIDE.flush_buffers()
       case None =>
     }