# HG changeset patch
# User wenzelm
# Date 1483806606 -3600
# Node ID 37bf7acf6a4bfaf03ad8b03ad933b302ce123e80
# Parent  00488a8c042f668c8e9b9563bd6b976e94ac8bbb
clarified lazy text content;

diff -r 00488a8c042f -r 37bf7acf6a4b src/Pure/PIDE/line.scala
--- a/src/Pure/PIDE/line.scala	Sat Jan 07 16:16:41 2017 +0100
+++ b/src/Pure/PIDE/line.scala	Sat Jan 07 17:30:06 2017 +0100
@@ -95,9 +95,17 @@
 
   sealed case class Document(lines: List[Line], text_length: Text.Length)
   {
-    def make_text: String = lines.mkString("", "\n", "")
+    lazy val text: String = lines.mkString("", "\n", "")
+    lazy val bytes: Bytes = Bytes(text)
+    lazy val chunk: Symbol.Text_Chunk = Symbol.Text_Chunk(text)
 
-    override def toString: String = make_text
+    lazy val length: Int =
+      if (lines.isEmpty) 0
+      else ((0 /: lines) { case (n, line) => n + line.text.length + 1 }) - 1
+
+    def text_range: Text.Range = Text.Range(0, length)
+
+    override def toString: String = text
 
     override def equals(that: Any): Boolean =
       that match {
@@ -136,18 +144,6 @@
       }
       else None
     }
-
-    lazy val length: Int =
-      if (lines.isEmpty) 0
-      else ((0 /: lines) { case (n, line) => n + line.text.length + 1 }) - 1
-
-    def full_range: Text.Range = Text.Range(0, length)
-
-    lazy val blob: (Bytes, Symbol.Text_Chunk) =
-    {
-      val text = make_text
-      (Bytes(text), Symbol.Text_Chunk(text))
-    }
   }
 
 
diff -r 00488a8c042f -r 37bf7acf6a4b src/Tools/VSCode/src/document_model.scala
--- a/src/Tools/VSCode/src/document_model.scala	Sat Jan 07 16:16:41 2017 +0100
+++ b/src/Tools/VSCode/src/document_model.scala	Sat Jan 07 17:30:06 2017 +0100
@@ -76,18 +76,14 @@
 
   def get_blob: Option[Document.Blob] =
     if (is_theory) None
-    else {
-      val (bytes, chunk) = doc.blob
-      val changed = pending_edits.nonEmpty
-      Some((Document.Blob(bytes, chunk, changed)))
-    }
+    else Some((Document.Blob(doc.bytes, doc.chunk, pending_edits.nonEmpty)))
 
 
   /* edits */
 
   def update_text(text: String): Option[Document_Model] =
   {
-    val old_text = doc.make_text
+    val old_text = doc.text
     val new_text = Line.normalize(text)
     Text.Edit.replace(0, old_text, new_text) match {
       case Nil => None
diff -r 00488a8c042f -r 37bf7acf6a4b src/Tools/VSCode/src/server.scala
--- a/src/Tools/VSCode/src/server.scala	Sat Jan 07 16:16:41 2017 +0100
+++ b/src/Tools/VSCode/src/server.scala	Sat Jan 07 17:30:06 2017 +0100
@@ -315,7 +315,7 @@
       (for ((rendering, offset) <- rendering_offset(node_pos))
         yield {
           val doc = rendering.model.doc
-          rendering.caret_focus_ranges(Text.Range(offset, offset + 1), doc.full_range)
+          rendering.caret_focus_ranges(Text.Range(offset, offset + 1), doc.text_range)
             .map(r => Protocol.DocumentHighlight.text(doc.range(r)))
         }) getOrElse Nil
     channel.write(Protocol.DocumentHighlights.reply(id, result))
diff -r 00488a8c042f -r 37bf7acf6a4b src/Tools/VSCode/src/vscode_rendering.scala
--- a/src/Tools/VSCode/src/vscode_rendering.scala	Sat Jan 07 16:16:41 2017 +0100
+++ b/src/Tools/VSCode/src/vscode_rendering.scala	Sat Jan 07 17:30:06 2017 +0100
@@ -47,7 +47,7 @@
 
   def diagnostics: List[Text.Info[Command.Results]] =
     snapshot.cumulate[Command.Results](
-      model.doc.full_range, Command.Results.empty, VSCode_Rendering.diagnostics_elements, _ =>
+      model.doc.text_range, Command.Results.empty, VSCode_Rendering.diagnostics_elements, _ =>
       {
         case (res, Text.Info(_, msg @ XML.Elem(Markup(_, Markup.Serial(i)), body)))
         if body.nonEmpty => Some(res + (i -> msg))
diff -r 00488a8c042f -r 37bf7acf6a4b src/Tools/VSCode/src/vscode_resources.scala
--- a/src/Tools/VSCode/src/vscode_resources.scala	Sat Jan 07 16:16:41 2017 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Sat Jan 07 17:30:06 2017 +0100
@@ -72,7 +72,7 @@
     val file = node_file(name)
     get_model(file) match {
       case Some(model) =>
-        f(new CharSequenceReader(model.doc.make_text))
+        f(new CharSequenceReader(model.doc.text))
       case None if file.isFile =>
         val reader = Scan.byte_reader(file)
         try { f(reader) } finally { reader.close }
@@ -139,7 +139,7 @@
 
   def get_file_content(file: JFile): Option[String] =
     get_model(file) match {
-      case Some(model) => Some(model.doc.make_text)
+      case Some(model) => Some(model.doc.text)
       case None => read_file_content(file)
     }