explicit Status.REMOVED, which is required e.g. for sledgehammer to retrieve command of sendback exec_id (in contrast to find_theorems, see c2da0d3b974d);

--- a/src/Pure/PIDE/query_operation.scala	Wed Sep 25 10:26:04 2013 +0200
+++ b/src/Pure/PIDE/query_operation.scala	Wed Sep 25 11:12:59 2013 +0200
@@ -18,6 +18,7 @@
     val WAITING = Value("waiting")
     val RUNNING = Value("running")
     val FINISHED = Value("finished")
+    val REMOVED = Value("removed")
   }
 }
 
@@ -37,7 +38,7 @@
   private var current_query: List[String] = Nil
   private var current_update_pending = false
   private var current_output: List[XML.Tree] = Nil
-  private var current_status = Query_Operation.Status.FINISHED
+  private var current_status = Query_Operation.Status.REMOVED
   private var current_exec_id = Document_ID.none
 
   private def reset_state()
@@ -46,7 +47,7 @@
     current_query = Nil
     current_update_pending = false
     current_output = Nil
-    current_status = Query_Operation.Status.FINISHED
+    current_status = Query_Operation.Status.REMOVED
     current_exec_id = Document_ID.none
   }
 
@@ -100,7 +101,7 @@
       results.collectFirst({ case XML.Elem(_, List(elem: XML.Elem)) if elem.name == name => status })
 
     val new_status =
-      if (removed) Query_Operation.Status.FINISHED
+      if (removed) Query_Operation.Status.REMOVED
       else
         get_status(Markup.FINISHED, Query_Operation.Status.FINISHED) orElse
         get_status(Markup.RUNNING, Query_Operation.Status.RUNNING) getOrElse
@@ -128,7 +129,7 @@
         if (current_status != new_status) {
           current_status = new_status
           consume_status(new_status)
-          if (new_status == Query_Operation.Status.FINISHED) {
+          if (new_status == Query_Operation.Status.REMOVED) {
             remove_overlay()
             editor.flush()
           }
@@ -187,7 +188,7 @@
           current_location match {
             case Some(command)
             if current_update_pending ||
-              (current_status != Query_Operation.Status.FINISHED &&
+              (current_status != Query_Operation.Status.REMOVED &&
                 changed.commands.contains(command)) =>
               Swing_Thread.later { content_update() }
             case _ =>

--- a/src/Tools/jEdit/src/find_dockable.scala	Wed Sep 25 10:26:04 2013 +0200
+++ b/src/Tools/jEdit/src/find_dockable.scala	Wed Sep 25 11:12:59 2013 +0200
@@ -37,7 +37,7 @@
         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 =>
+      case _ =>
         process_indicator.update(null, 0)
     }
   }

--- a/src/Tools/jEdit/src/sledgehammer_dockable.scala	Wed Sep 25 10:26:04 2013 +0200
+++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala	Wed Sep 25 11:12:59 2013 +0200
@@ -38,7 +38,7 @@
         process_indicator.update("Waiting for evaluation of context ...", 5)
       case Query_Operation.Status.RUNNING =>
         process_indicator.update("Sledgehammering ...", 15)
-      case Query_Operation.Status.FINISHED =>
+      case _ =>
         process_indicator.update(null, 0)
     }
   }