--- a/src/Pure/PIDE/query_operation.scala Mon Sep 21 11:45:03 2015 +0200
+++ b/src/Pure/PIDE/query_operation.scala Mon Sep 21 13:53:35 2015 +0200
@@ -25,6 +25,7 @@
consume_status: Query_Operation.Status.Value => Unit,
consume_output: (Document.Snapshot, Command.Results, XML.Body) => Unit)
{
+ private val print_function = operation_name + "_query"
private val instance = Document_ID.make().toString
@@ -52,7 +53,7 @@
current_location match {
case None =>
case Some(command) =>
- editor.remove_overlay(command, operation_name, instance :: current_query)
+ editor.remove_overlay(command, print_function, instance :: current_query)
editor.flush()
}
}
@@ -184,7 +185,7 @@
current_location = Some(command)
current_query = query
current_status = Query_Operation.Status.WAITING
- editor.insert_overlay(command, operation_name, instance :: query)
+ editor.insert_overlay(command, print_function, instance :: query)
case None =>
}
}