more robust Windows support;
authorwenzelm
Sun Dec 10 14:45:12 2017 +0100 (17 months ago)
changeset 67174258e1394e76a
parent 67173 e746db6db903
child 67175 4e5ba4b23731
more robust Windows support;
src/Pure/Thy/latex.scala
     1.1 --- a/src/Pure/Thy/latex.scala	Sun Dec 10 14:29:14 2017 +0100
     1.2 +++ b/src/Pure/Thy/latex.scala	Sun Dec 10 14:45:12 2017 +0100
     1.3 @@ -23,7 +23,7 @@
     1.4    private val Range_Pattern1 = """^.*%:%range=(\d+)%:%$""".r
     1.5  
     1.6    def read_tex_file(tex_file: Path): Tex_File =
     1.7 -    new Tex_File(tex_file, split_lines(File.read(tex_file)).toArray)
     1.8 +    new Tex_File(tex_file, Line.logical_lines(File.read(tex_file)).toArray)
     1.9  
    1.10    final class Tex_File private[Latex](val tex_file: Path, tex_lines: Array[String])
    1.11    {
    1.12 @@ -142,7 +142,7 @@
    1.13        }
    1.14      }
    1.15  
    1.16 -    filter(split_lines(root_log), Nil)
    1.17 +    filter(Line.logical_lines(root_log), Nil)
    1.18    }
    1.19  
    1.20