src/Pure/PIDE/query_operation.scala
changeset 61206 d5aeb401111a
parent 60893 3c8b9b4b577c
child 61210 a3a05d734858
--- 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 =>
           }
         }