diff -r 48ff625687f5 -r 55cb4271858b src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Fri Apr 03 13:51:56 2020 +0200
+++ b/src/Pure/PIDE/command.ML	Fri Apr 03 17:35:10 2020 +0200
@@ -58,7 +58,9 @@
 
 fun read_file_node file_node master_dir pos src_path =
   let
-    val _ = Position.report pos Markup.language_path;
+    val _ =
+      if Context_Position.pide_reports ()
+      then Position.report pos Markup.language_path else ();
     val _ =
       (case try Url.explode file_node of
         NONE => ()