# HG changeset patch
# User wenzelm
# Date 1442836415 -7200
# Node ID d5aeb401111a328eb55dbe5c20ced4a4ccc7ab9f
# Parent  c0a5ebecc68b447171697abf2cf53cb025d36774
more specific name to reduce danger of clash with direct uses of plain Command.print_function;

diff -r c0a5ebecc68b -r d5aeb401111a src/Pure/PIDE/query_operation.ML
--- 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;
-
diff -r c0a5ebecc68b -r d5aeb401111a src/Pure/PIDE/query_operation.scala
--- 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 =>
           }
         }