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 => ()