src/Pure/PIDE/command.ML
changeset 71675 55cb4271858b
parent 70662 0f9a4e8ee1ab
child 72747 5f9d66155081
--- 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 => ()