# HG changeset patch
# User wenzelm
# Date 1661714728 -7200
# Node ID 28445a0bd86943dd92488558ebb8292c0d177d96
# Parent  63b22e3b80183687b07e1771e297496ba05eb83a
more markup (for batch build);

diff -r 63b22e3b8018 -r 28445a0bd869 src/Pure/PIDE/resources.ML
--- a/src/Pure/PIDE/resources.ML	Sun Aug 28 20:21:47 2022 +0200
+++ b/src/Pure/PIDE/resources.ML	Sun Aug 28 21:25:28 2022 +0200
@@ -330,6 +330,10 @@
           val pos = Input.pos_of source;
           val delimited = Input.is_delimited source;
           val src_paths = make_paths (Path.explode name);
+          val reports =
+            src_paths |> map (fn src_path =>
+              (pos, Markup.path (Path.implode_symbolic (master_dir + src_path))));
+          val _ = Position.reports reports;
         in map (Command.read_file master_dir pos delimited) src_paths end
     | files => map Exn.release files));