proper file;
authorwenzelm
Mon Dec 11 17:49:47 2017 +0100 (17 months ago)
changeset 6718328227b13a2f1
parent 67182 bdc03e20fce3
child 67184 ecc786cb3b7b
proper file;
src/Pure/Thy/latex.scala
     1.1 --- a/src/Pure/Thy/latex.scala	Mon Dec 11 14:10:41 2017 +0100
     1.2 +++ b/src/Pure/Thy/latex.scala	Mon Dec 11 17:49:47 2017 +0100
     1.3 @@ -118,7 +118,7 @@
     1.4            case Pattern(file, Value.Int(line), message) =>
     1.5              val path = File.standard_path(file)
     1.6              if (Path.is_wellformed(path)) {
     1.7 -              val file = dir + Path.explode(path)
     1.8 +              val file = (dir + Path.explode(path)).canonical
     1.9                if (file.is_file) Some((file, line, message)) else None
    1.10              }
    1.11              else None
    1.12 @@ -141,7 +141,7 @@
    1.13      {
    1.14        lines match {
    1.15          case File_Line_Error((file, line, msg1)) :: rest1 =>
    1.16 -          val pos = tex_file_position((dir + file).canonical, line)
    1.17 +          val pos = tex_file_position(file, line)
    1.18            rest1 match {
    1.19              case Line_Error((line2, msg2)) :: rest2 if line == line2 =>
    1.20                filter(rest2, (Exn.cat_message(msg1, msg2), pos) :: result)