# HG changeset patch
# User wenzelm
# Date 1375818084 -7200
# Node ID 8069c8b9335ecf8eb143bd7fd2e1b4ff2a7bb4b2
# Parent  9a26ec5739dd633bedbd792235189448a1fd6d7a
more tooltips;

diff -r 9a26ec5739dd -r 8069c8b9335e src/Tools/jEdit/src/query_operation.scala
--- a/src/Tools/jEdit/src/query_operation.scala	Tue Aug 06 21:34:58 2013 +0200
+++ b/src/Tools/jEdit/src/query_operation.scala	Tue Aug 06 21:41:24 2013 +0200
@@ -87,9 +87,17 @@
   private def animation_update()
   {
     animation_icon.stop
-    if (current_status != Status.FINISHED) {
-      animation_icon.setRate(if (current_status == Status.RUNNING) 15 else 5)
-      animation_icon.start
+    current_status match {
+      case Status.WAITING =>
+        animation.tooltip = "Waiting for evaluation of query context ..."
+        animation_icon.setRate(5)
+        animation_icon.start
+      case Status.RUNNING =>
+        animation.tooltip = "Running query operation ..."
+        animation_icon.setRate(15)
+        animation_icon.start
+      case Status.FINISHED =>
+        animation.tooltip = null
     }
   }