src/Pure/PIDE/query_operation.scala
changeset 53844 71f103629327
parent 53840 75243ba102d4
child 53872 6e69f9ca8f1c
     1.1 --- a/src/Pure/PIDE/query_operation.scala	Tue Sep 24 16:06:12 2013 +0200
     1.2 +++ b/src/Pure/PIDE/query_operation.scala	Tue Sep 24 16:35:01 2013 +0200
     1.3 @@ -153,7 +153,7 @@
     1.4          reset_state()
     1.5          consume_output(Document.Snapshot.init, Command.Results.empty, Nil)
     1.6          editor.current_command(editor_context, snapshot) match {
     1.7 -          case Some((command, _)) =>
     1.8 +          case Some(command) =>
     1.9              current_location = Some(command)
    1.10              current_query = query
    1.11              current_status = Query_Operation.Status.WAITING