more accurate position for auxiliary files;
authorwenzelm
Thu Aug 30 19:52:30 2018 +0200 (13 months ago)
changeset 68858e1796b8ddbae
parent 68857 b888de4fe58c
child 68859 9207ada0ca31
more accurate position for auxiliary files;
src/Pure/General/position.ML
src/Pure/PIDE/command.ML
     1.1 --- a/src/Pure/General/position.ML	Thu Aug 30 17:24:43 2018 +0200
     1.2 +++ b/src/Pure/General/position.ML	Thu Aug 30 19:52:30 2018 +0200
     1.3 @@ -29,6 +29,7 @@
     1.4    val id_only: string -> T
     1.5    val get_id: T -> string option
     1.6    val put_id: string -> T -> T
     1.7 +  val copy_id: T -> T -> T
     1.8    val id_properties_of: T -> Properties.T
     1.9    val parse_id: T -> int option
    1.10    val adjust_offsets: (int -> int option) -> T -> T
    1.11 @@ -142,6 +143,7 @@
    1.12  
    1.13  fun get_id (Pos (_, props)) = Properties.get props Markup.idN;
    1.14  fun put_id id (Pos (count, props)) = Pos (count, norm_props (Properties.put (Markup.idN, id) props));
    1.15 +fun copy_id pos = (case get_id pos of NONE => I | SOME id => put_id id);
    1.16  
    1.17  fun parse_id pos = Option.map Value.parse_int (get_id pos);
    1.18  
    1.19 @@ -151,14 +153,16 @@
    1.20    | NONE => []);
    1.21  
    1.22  fun adjust_offsets adjust (pos as Pos (_, props)) =
    1.23 -  (case parse_id pos of
    1.24 -    SOME id =>
    1.25 -      (case adjust id of
    1.26 -        SOME offset =>
    1.27 -          let val Pos (count, _) = advance_offsets offset pos
    1.28 -          in Pos (count, Properties.remove Markup.idN props) end
    1.29 -      | NONE => pos)
    1.30 -  | NONE => pos);
    1.31 +  if is_none (file_of pos) then
    1.32 +    (case parse_id pos of
    1.33 +      SOME id =>
    1.34 +        (case adjust id of
    1.35 +          SOME offset =>
    1.36 +            let val Pos (count, _) = advance_offsets offset pos
    1.37 +            in Pos (count, Properties.remove Markup.idN props) end
    1.38 +        | NONE => pos)
    1.39 +    | NONE => pos)
    1.40 +  else pos;
    1.41  
    1.42  
    1.43  (* markup properties *)
     2.1 --- a/src/Pure/PIDE/command.ML	Thu Aug 30 17:24:43 2018 +0200
     2.2 +++ b/src/Pure/PIDE/command.ML	Thu Aug 30 19:52:30 2018 +0200
     2.3 @@ -70,7 +70,8 @@
     2.4      val text = File.read full_path;
     2.5      val lines = split_lines text;
     2.6      val digest = SHA1.digest text;
     2.7 -  in {src_path = src_path, lines = lines, digest = digest, pos = Path.position full_path} end
     2.8 +    val file_pos = Position.copy_id pos (Path.position full_path);
     2.9 +  in {src_path = src_path, lines = lines, digest = digest, pos = file_pos} end
    2.10    handle ERROR msg => error (msg ^ Position.here pos);
    2.11  
    2.12  val read_file = read_file_node "";