# HG changeset patch # User wenzelm # Date 1380100379 -7200 # Node ID 6e69f9ca8f1c80a1a8d3e00c83ee73ef930a89f0 # Parent 7c23df53af01a5ae339c87f71443b43c08865213 explicit Status.REMOVED, which is required e.g. for sledgehammer to retrieve command of sendback exec_id (in contrast to find_theorems, see c2da0d3b974d); diff -r 7c23df53af01 -r 6e69f9ca8f1c src/Pure/PIDE/query_operation.scala --- 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 _ => diff -r 7c23df53af01 -r 6e69f9ca8f1c src/Tools/jEdit/src/find_dockable.scala --- 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) } } diff -r 7c23df53af01 -r 6e69f9ca8f1c src/Tools/jEdit/src/sledgehammer_dockable.scala --- 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) } }