# HG changeset patch
# User wenzelm
# Date 1512913512 -3600
# Node ID 258e1394e76afc70d1bab28a9871ded8ab37419e
# Parent  e746db6db903732d6425d17300fe402ac58db182
more robust Windows support;

diff -r e746db6db903 -r 258e1394e76a src/Pure/Thy/latex.scala
--- a/src/Pure/Thy/latex.scala	Sun Dec 10 14:29:14 2017 +0100
+++ b/src/Pure/Thy/latex.scala	Sun Dec 10 14:45:12 2017 +0100
@@ -23,7 +23,7 @@
   private val Range_Pattern1 = """^.*%:%range=(\d+)%:%$""".r
 
   def read_tex_file(tex_file: Path): Tex_File =
-    new Tex_File(tex_file, split_lines(File.read(tex_file)).toArray)
+    new Tex_File(tex_file, Line.logical_lines(File.read(tex_file)).toArray)
 
   final class Tex_File private[Latex](val tex_file: Path, tex_lines: Array[String])
   {
@@ -142,7 +142,7 @@
       }
     }
 
-    filter(split_lines(root_log), Nil)
+    filter(Line.logical_lines(root_log), Nil)
   }