# HG changeset patch
# User wenzelm
# Date 1375739849 -7200
# Node ID 91032244e4caded284e4ac844ff3b96b42cf75ab
# Parent  9e934d4fff0072b0569f136f1b8f5d6b10eb2a06
query process animation;

diff -r 9e934d4fff00 -r 91032244e4ca src/Tools/jEdit/etc/options
--- a/src/Tools/jEdit/etc/options	Mon Aug 05 22:54:50 2013 +0200
+++ b/src/Tools/jEdit/etc/options	Mon Aug 05 23:57:29 2013 +0200
@@ -83,4 +83,6 @@
 option gutter_warning_icon : string = "idea-icons/runConfigurations/testFailed.png"
 option gutter_legacy_icon : string = "idea-icons/general/balloonWarning.png"
 option gutter_error_icon : string = "idea-icons/runConfigurations/testError.png"
+option process_passive_icon : string = "idea-icons/process/step_passive.png"
+option process_active_icons : string = "idea-icons/process/step_1.png:idea-icons/process/step_2.png:idea-icons/process/step_3.png:idea-icons/process/step_4.png:idea-icons/process/step_5.png:idea-icons/process/step_6.png:idea-icons/process/step_7.png:idea-icons/process/step_8.png:idea-icons/process/step_9.png:idea-icons/process/step_10.png:idea-icons/process/step_11.png:idea-icons/process/step_12.png"
 
diff -r 9e934d4fff00 -r 91032244e4ca src/Tools/jEdit/src/find_dockable.scala
--- a/src/Tools/jEdit/src/find_dockable.scala	Mon Aug 05 22:54:50 2013 +0200
+++ b/src/Tools/jEdit/src/find_dockable.scala	Mon Aug 05 23:57:29 2013 +0200
@@ -114,6 +114,7 @@
   }
 
   private val controls =
-    new FlowPanel(FlowPanel.Alignment.Right)(query_wrapped, find, locate, zoom)
+    new FlowPanel(FlowPanel.Alignment.Right)(
+      query_wrapped, find_theorems.animation, find, locate, zoom)
   add(controls.peer, BorderLayout.NORTH)
 }
diff -r 9e934d4fff00 -r 91032244e4ca src/Tools/jEdit/src/jedit_lib.scala
--- a/src/Tools/jEdit/src/jedit_lib.scala	Mon Aug 05 22:54:50 2013 +0200
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Mon Aug 05 23:57:29 2013 +0200
@@ -10,7 +10,7 @@
 import isabelle._
 
 import java.awt.{Component, Container, Window, GraphicsEnvironment, Point, Rectangle}
-import javax.swing.Icon
+import javax.swing.{Icon, ImageIcon}
 
 import scala.annotation.tailrec
 
@@ -240,5 +240,11 @@
     if (icon.getIconWidth < 0 || icon.getIconHeight < 0) error("Bad icon: " + name)
     else icon
   }
+
+  def load_image_icon(name: String): ImageIcon =
+    load_icon(name) match {
+      case icon: ImageIcon => icon
+      case _ => error("Bad image icon: " + name)
+    }
 }
 
diff -r 9e934d4fff00 -r 91032244e4ca src/Tools/jEdit/src/query_operation.scala
--- a/src/Tools/jEdit/src/query_operation.scala	Mon Aug 05 22:54:50 2013 +0200
+++ b/src/Tools/jEdit/src/query_operation.scala	Mon Aug 05 23:57:29 2013 +0200
@@ -11,8 +11,10 @@
 import isabelle._
 
 import scala.actors.Actor._
+import scala.swing.Label
 
 import org.gjt.sp.jedit.View
+import org.gjt.sp.jedit.gui.AnimatedIcon
 
 
 object Query_Operation
@@ -32,6 +34,19 @@
   private val instance = Document_ID.make().toString
 
 
+  /* status animation */
+
+  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)
+
+  val animation = new Label
+  val animation_icon = new AnimatedIcon(passive_icon, active_icons.toArray, 10, animation.peer)
+  animation.icon = animation_icon
+
+
   /* implicit state -- owned by Swing thread */
 
   private var current_location: Option[Command] = None
@@ -81,6 +96,7 @@
 
     if (!new_output.isEmpty) {
       current_result = true
+      animation_icon.stop
       remove_overlay()
       PIDE.flush_buffers()
     }
@@ -101,6 +117,7 @@
         current_location = None
         current_query = Nil
         current_result = false
+        animation_icon.start
         snapshot.node.command_at(doc_view.text_area.getCaretPosition).map(_._1) match {
           case Some(command) =>
             current_location = Some(command)