more specific name to reduce danger of clash with direct uses of plain Command.print_function;
authorwenzelm
Mon, 21 Sep 2015 13:53:35 +0200
changeset 61206 d5aeb401111a
parent 61205 c0a5ebecc68b
child 61207 46fa8f71e0ed
more specific name to reduce danger of clash with direct uses of plain Command.print_function;
src/Pure/PIDE/query_operation.ML
src/Pure/PIDE/query_operation.scala
--- 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 =>
           }
         }