# HG changeset patch
# User wenzelm
# Date 1513010987 -3600
# Node ID 28227b13a2f1b9d4de9dcd8a939df123f769ffee
# Parent  bdc03e20fce3b65f70ce7ba0d88331d3e675e798
proper file;

diff -r bdc03e20fce3 -r 28227b13a2f1 src/Pure/Thy/latex.scala
--- a/src/Pure/Thy/latex.scala	Mon Dec 11 14:10:41 2017 +0100
+++ b/src/Pure/Thy/latex.scala	Mon Dec 11 17:49:47 2017 +0100
@@ -118,7 +118,7 @@
           case Pattern(file, Value.Int(line), message) =>
             val path = File.standard_path(file)
             if (Path.is_wellformed(path)) {
-              val file = dir + Path.explode(path)
+              val file = (dir + Path.explode(path)).canonical
               if (file.is_file) Some((file, line, message)) else None
             }
             else None
@@ -141,7 +141,7 @@
     {
       lines match {
         case File_Line_Error((file, line, msg1)) :: rest1 =>
-          val pos = tex_file_position((dir + file).canonical, line)
+          val pos = tex_file_position(file, line)
           rest1 match {
             case Line_Error((line2, msg2)) :: rest2 if line == line2 =>
               filter(rest2, (Exn.cat_message(msg1, msg2), pos) :: result)