src/Pure/Thy/latex.scala

   private val File_Pattern = """^.*%:%file=(.+)%:%$""".r
   private val Range_Pattern2 = """^.*%:%range=(\d+):(\d+)%:%$""".r
   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])
   {
     override def toString: String = tex_file.toString
 

         case _ :: rest => filter(rest, result)
         case Nil => result.reverse
       }
     }
 
-    filter(split_lines(root_log), Nil)
+    filter(Line.logical_lines(root_log), Nil)
   }
 
 
   /* errors */