--- 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 {
--- 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) {