src/Pure/PIDE/query_operation.scala
changeset 61210 a3a05d734858
parent 61206 d5aeb401111a
child 61545 57000ac6291f
--- 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