more specific name to reduce danger of clash with direct uses of plain Command.print_function;
--- a/src/Pure/PIDE/query_operation.ML Mon Sep 21 11:45:03 2015 +0200
+++ b/src/Pure/PIDE/query_operation.ML Mon Sep 21 13:53:35 2015 +0200
@@ -15,7 +15,7 @@
struct
fun register {name, pri} f =
- Command.print_function name
+ Command.print_function (name ^ "_query")
(fn {args = instance :: args, ...} =>
SOME {delay = NONE, pri = pri, persistent = false, strict = false,
print_fn = fn _ => uninterruptible (fn restore_attributes => fn state =>
@@ -37,4 +37,3 @@
| _ => NONE);
end;
-
--- 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 =>
}
}