src/Tools/jEdit/src/find_dockable.scala

--- a/src/Tools/jEdit/src/find_dockable.scala	Fri Aug 09 13:37:51 2013 +0200
+++ b/src/Tools/jEdit/src/find_dockable.scala	Fri Aug 09 13:51:34 2013 +0200
@@ -31,8 +31,22 @@
 
   /* query operation */
 
+  private val process_indicator = new Process_Indicator
+
+  private def consume_status(status: Query_Operation.Status.Value)
+  {
+    status match {
+      case Query_Operation.Status.WAITING =>
+        process_indicator.update("Waiting for evaluation of context ...", 5)
+      case Query_Operation.Status.RUNNING =>
+        process_indicator.update("Running find operation ...", 15)
+      case Query_Operation.Status.FINISHED =>
+        process_indicator.update(null, 0)
+    }
+  }
+
   private val find_theorems =
-    Query_Operation(view, "find_theorems",
+    Query_Operation(view, "find_theorems", consume_status _,
       (snapshot, results, body) =>
         pretty_text_area.update(snapshot, results, Pretty.separate(body)))
 
@@ -121,6 +135,6 @@
 
   private val controls =
     new FlowPanel(FlowPanel.Alignment.Right)(
-      query_wrapped, find_theorems.animation, apply_query, locate_query, zoom)
+      query_wrapped, process_indicator.component, apply_query, locate_query, zoom)
   add(controls.peer, BorderLayout.NORTH)
 }