# HG changeset patch
# User wenzelm
# Date 1482755317 -3600
# Node ID d8e0619abb60494eded4f935eeb6d9e168b17c69
# Parent  93e375bd3283cd4a37d5680d715b0ca48768b803
clarified document: no stored text;

diff -r 93e375bd3283 -r d8e0619abb60 src/Pure/PIDE/line.scala
--- a/src/Pure/PIDE/line.scala	Mon Dec 26 13:21:08 2016 +0100
+++ b/src/Pure/PIDE/line.scala	Mon Dec 26 13:28:37 2016 +0100
@@ -80,22 +80,25 @@
 
   object Document
   {
-    val empty: Document = new Document("", Nil)
+    val empty: Document = new Document(Nil)
 
     def apply(lines: List[Line]): Document =
       if (lines.isEmpty) empty
-      else new Document(lines.mkString("", "\n", ""), lines)
+      else new Document(lines)
 
     def apply(text: String): Document =
-      if (text.contains('\r'))
-        apply(Library.cat_lines(Library.split_lines(text).map(Library.trim_line(_))))
-      else if (text == "") Document.empty
-      else new Document(text, Library.split_lines(text).map(Line(_)))
+      if (text == "") empty
+      else if (text.contains('\r'))
+        new Document(Library.split_lines(text).map(s => Line(Library.trim_line(s))))
+      else
+        new Document(Library.split_lines(text).map(s => Line(s)))
   }
 
-  final class Document private(val text: String, val lines: List[Line])
+  final class Document private(val lines: List[Line])
   {
-    override def toString: String = text
+    def make_text: String = lines.mkString("", "\n", "")
+
+    override def toString: String = make_text
 
     override def equals(that: Any): Boolean =
       that match {
diff -r 93e375bd3283 -r d8e0619abb60 src/Tools/VSCode/src/document_model.scala
--- a/src/Tools/VSCode/src/document_model.scala	Mon Dec 26 13:21:08 2016 +0100
+++ b/src/Tools/VSCode/src/document_model.scala	Mon Dec 26 13:28:37 2016 +0100
@@ -30,7 +30,7 @@
   /* edits */
 
   def text_edits: List[Text.Edit] =
-    if (changed) List(Text.Edit.insert(0, doc.text)) else Nil
+    if (changed) List(Text.Edit.insert(0, doc.make_text)) else Nil
 
   def node_edits: List[Document.Edit_Text] =
     if (changed) {