# HG changeset patch
# User wenzelm
# Date 1483648444 -3600
# Node ID 99f49258b02bb65d53418a3b770c1f0396f43bd8
# Parent  d868f5c7a31c8f91cea86ac266a4a34823894075
more robust treatment of logical lines;

diff -r d868f5c7a31c -r 99f49258b02b src/Pure/PIDE/line.scala
--- a/src/Pure/PIDE/line.scala	Thu Jan 05 16:46:01 2017 +0100
+++ b/src/Pure/PIDE/line.scala	Thu Jan 05 21:34:04 2017 +0100
@@ -12,6 +12,15 @@
 
 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
@@ -34,7 +43,7 @@
     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)
@@ -81,10 +90,7 @@
   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)
diff -r d868f5c7a31c -r 99f49258b02b src/Tools/VSCode/src/document_model.scala
--- a/src/Tools/VSCode/src/document_model.scala	Thu Jan 05 16:46:01 2017 +0100
+++ b/src/Tools/VSCode/src/document_model.scala	Thu Jan 05 21:34:04 2017 +0100
@@ -92,8 +92,9 @@
 
   /* edits */
 
-  def update_text(new_text: String): Option[Document_Model] =
+  def update_text(text: String): Option[Document_Model] =
   {
+    val new_text = Line.normalize(text)
     val old_text = doc.make_text
     if (new_text == old_text) None
     else {
diff -r d868f5c7a31c -r 99f49258b02b src/Tools/VSCode/src/vscode_resources.scala
--- a/src/Tools/VSCode/src/vscode_resources.scala	Thu Jan 05 16:46:01 2017 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Thu Jan 05 21:34:04 2017 +0100
@@ -134,7 +134,7 @@
   /* file content */
 
   def try_read(file: JFile): Option[String] =
-    try { Some(File.read(file)) }
+    try { Some(Line.normalize(File.read(file))) }
     catch { case ERROR(_) => None }
 
   def get_file_content(file: JFile): Option[String] =