src/Pure/PIDE/line.scala

 import scala.annotation.tailrec
 
 
 object Line
 {
+  /* logical lines */
+
+  def normalize(text: String): String =
+    if (text.contains('\r')) text.replace("\r\n", "\n") else text
+
+  def logical_lines(text: String): List[String] =
+    Library.split_lines(normalize(text))
+
+
   /* position */
 
   object Position
   {
     val zero: Position = Position()

       }
 
     def advance(text: String, text_length: Text.Length): Position =
       if (text.isEmpty) this
       else {
-        val lines = Library.split_lines(text)
+        val lines = logical_lines(text)
         val l = line + lines.length - 1
         val c = (if (l == line) column else 0) + text_length(Library.trim_line(lines.last))
         Position(l, c)
       }
   }

   /* document with newline as separator (not terminator) */
 
   object Document
   {
     def apply(text: String, text_length: Text.Length): Document =
-      if (text.contains('\r'))
-        Document(Library.split_lines(text).map(s => Line(Library.trim_line(s))), text_length)
-      else
-        Document(Library.split_lines(text).map(s => Line(s)), text_length)
+      Document(logical_lines(text).map(Line(_)), text_length)
   }
 
   sealed case class Document(lines: List[Line], text_length: Text.Length)
   {
     def make_text: String = lines.mkString("", "\n", "")