--- 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 "";