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