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