# HG changeset patch
# User wenzelm
# Date 1399553584 -7200
# Node ID a1557dc7f589d32195359ace27ea3a2833eeac5a
# Parent  734f7e6151c9ecf43833f923bbadd073b8380241
tuned GUI;

diff -r 734f7e6151c9 -r a1557dc7f589 src/Tools/jEdit/src/query_dockable.scala
--- a/src/Tools/jEdit/src/query_dockable.scala	Thu May 08 13:47:17 2014 +0200
+++ b/src/Tools/jEdit/src/query_dockable.scala	Thu May 08 14:53:04 2014 +0200
@@ -91,7 +91,7 @@
       query_operation.apply_query(List(limit.text, allow_dups.selected.toString, query.getText))
     }
 
-    private val query_label = new Label("Query:") {
+    private val query_label = new Label("Find:") {
       tooltip =
         GUI.tooltip_lines(
           "Search criteria for find operation, e.g.\n\"_ = _\" \"op +\" name: Group -name: monoid")
@@ -155,7 +155,7 @@
       query_operation.apply_query(List(query.getText))
     }
 
-    private val query_label = new Label("Query:") {
+    private val query_label = new Label("Find:") {
       tooltip = GUI.tooltip_lines("Name / type patterns for constants")
     }
 
@@ -190,8 +190,11 @@
   {
     /* query */
 
+    private val process_indicator = new Process_Indicator
+
     val query_operation =
-      new Query_Operation(PIDE.editor, view, "print_operation", _ => (),
+      new Query_Operation(PIDE.editor, view, "print_operation",
+        consume_status(process_indicator, _),
         (snapshot, results, body) =>
           pretty_text_area.update(snapshot, results, Pretty.separate(body)))
 
@@ -257,7 +260,7 @@
       set_selector()
       control_panel.contents.clear
       control_panel.contents ++=
-        List(query_label, selector, apply_button,
+        List(query_label, selector, process_indicator.component, apply_button,
           pretty_text_area.search_label, pretty_text_area.search_pattern, zoom)
     }