author | wenzelm |
Wed, 28 Dec 2022 16:14:37 +0100 | |
changeset 76805 | 5a28de3388cd |
parent 76804 | 3e8340fcaa16 |
child 76806 | 797621be9317 |
--- a/src/Pure/PIDE/resources.ML Wed Dec 28 16:13:08 2022 +0100 +++ b/src/Pure/PIDE/resources.ML Wed Dec 28 16:14:37 2022 +0100 @@ -332,9 +332,7 @@ fun read_file_node file_node master_dir pos delimited src_path = let - val _ = - if Context_Position.reports_enabled0 () - then Position.report pos (Markup.language_path delimited) else (); + val _ = Position.report pos (Markup.language_path delimited); fun read_local () = let