# HG changeset patch # User wenzelm # Date 1512997841 -3600 # Node ID bdc03e20fce3b65f70ce7ba0d88331d3e675e798 # Parent 0da2811afd8702db9d939b936d7a8b0718748d3c clarified file positions; diff -r 0da2811afd87 -r bdc03e20fce3 src/Pure/Thy/latex.scala --- a/src/Pure/Thy/latex.scala Mon Dec 11 14:10:12 2017 +0100 +++ b/src/Pure/Thy/latex.scala Mon Dec 11 14:10:41 2017 +0100 @@ -79,7 +79,7 @@ } def tex_position(line: Int): Position.T = - Position.File(tex_file.implode) ::: Position.Line(line) + Position.Line_File(line, tex_file.implode) def position(line: Int): Position.T = source_position(line) getOrElse tex_position(line) @@ -141,7 +141,7 @@ { lines match { case File_Line_Error((file, line, msg1)) :: rest1 => - val pos = tex_file_position(file, line) + val pos = tex_file_position((dir + file).canonical, line) rest1 match { case Line_Error((line2, msg2)) :: rest2 if line == line2 => filter(rest2, (Exn.cat_message(msg1, msg2), pos) :: result)