diff -r 7a421e7ef97c -r a3a05d734858 src/Pure/PIDE/query_operation.scala
--- a/src/Pure/PIDE/query_operation.scala	Mon Sep 21 15:07:23 2015 +0200
+++ b/src/Pure/PIDE/query_operation.scala	Mon Sep 21 15:55:29 2015 +0200
@@ -38,6 +38,8 @@
   @volatile private var current_status = Query_Operation.Status.FINISHED
   @volatile private var current_exec_id = Document_ID.none
 
+  def get_location: Option[Command] = current_location
+
   private def reset_state()
   {
     current_location = None