--- 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"
--- 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)
}
--- 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)
+ }
}
--- 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)