# HG changeset patch
# User wenzelm
# Date 1535651550 -7200
# Node ID e1796b8ddbae534055428c4fe898654a5ead6498
# Parent  b888de4fe58ca7b2f3b5a7aac9d76cc63a34e029
more accurate position for auxiliary files;

diff -r b888de4fe58c -r e1796b8ddbae src/Pure/General/position.ML
--- a/src/Pure/General/position.ML	Thu Aug 30 17:24:43 2018 +0200
+++ b/src/Pure/General/position.ML	Thu Aug 30 19:52:30 2018 +0200
@@ -29,6 +29,7 @@
   val id_only: string -> T
   val get_id: T -> string option
   val put_id: string -> T -> T
+  val copy_id: T -> T -> T
   val id_properties_of: T -> Properties.T
   val parse_id: T -> int option
   val adjust_offsets: (int -> int option) -> T -> T
@@ -142,6 +143,7 @@
 
 fun get_id (Pos (_, props)) = Properties.get props Markup.idN;
 fun put_id id (Pos (count, props)) = Pos (count, norm_props (Properties.put (Markup.idN, id) props));
+fun copy_id pos = (case get_id pos of NONE => I | SOME id => put_id id);
 
 fun parse_id pos = Option.map Value.parse_int (get_id pos);
 
@@ -151,14 +153,16 @@
   | NONE => []);
 
 fun adjust_offsets adjust (pos as Pos (_, props)) =
-  (case parse_id pos of
-    SOME id =>
-      (case adjust id of
-        SOME offset =>
-          let val Pos (count, _) = advance_offsets offset pos
-          in Pos (count, Properties.remove Markup.idN props) end
-      | NONE => pos)
-  | NONE => pos);
+  if is_none (file_of pos) then
+    (case parse_id pos of
+      SOME id =>
+        (case adjust id of
+          SOME offset =>
+            let val Pos (count, _) = advance_offsets offset pos
+            in Pos (count, Properties.remove Markup.idN props) end
+        | NONE => pos)
+    | NONE => pos)
+  else pos;
 
 
 (* markup properties *)
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 "";