diff -r b888de4fe58c -r e1796b8ddbae src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Thu Aug 30 17:24:43 2018 +0200
+++ b/src/Pure/PIDE/command.ML	Thu Aug 30 19:52:30 2018 +0200
@@ -70,7 +70,8 @@
     val text = File.read full_path;
     val lines = split_lines text;
     val digest = SHA1.digest text;
-  in {src_path = src_path, lines = lines, digest = digest, pos = Path.position full_path} end
+    val file_pos = Position.copy_id pos (Path.position full_path);
+  in {src_path = src_path, lines = lines, digest = digest, pos = file_pos} end
   handle ERROR msg => error (msg ^ Position.here pos);
 
 val read_file = read_file_node "";