more explocit Document_Model.Content;

--- a/src/Pure/PIDE/line.scala	Sun Jan 08 11:41:18 2017 +0100
+++ b/src/Pure/PIDE/line.scala	Sun Jan 08 12:00:37 2017 +0100
@@ -103,8 +103,6 @@
       Text.Range(0, length)
     }
     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 = text
 

--- a/src/Tools/VSCode/src/document_model.scala	Sun Jan 08 11:41:18 2017 +0100
+++ b/src/Tools/VSCode/src/document_model.scala	Sun Jan 08 12:00:37 2017 +0100
@@ -14,18 +14,26 @@
 
 object Document_Model
 {
+  sealed case class Content(doc: Line.Document)
+  {
+    def text_range: Text.Range = doc.text_range
+    def text: String = doc.text
+    lazy val bytes: Bytes = Bytes(text)
+    lazy val chunk: Symbol.Text_Chunk = Symbol.Text_Chunk(text)
+  }
+
   def init(session: Session, node_name: Document.Node.Name): Document_Model =
   {
     val resources = session.resources.asInstanceOf[VSCode_Resources]
-    val doc = Line.Document("", resources.text_length)
-    Document_Model(session, node_name, doc)
+    val content = Content(Line.Document("", resources.text_length))
+    Document_Model(session, node_name, content)
   }
 }
 
 sealed case class Document_Model(
   session: Session,
   node_name: Document.Node.Name,
-  doc: Line.Document,
+  content: Document_Model.Content,
   external_file: Boolean = false,
   node_required: Boolean = false,
   last_perspective: Document.Node.Perspective_Text = Document.Node.no_perspective_text,
@@ -43,7 +51,7 @@
 
   def node_header: Document.Node.Header =
     resources.special_header(node_name) getOrElse
-      resources.check_thy_reader("", node_name, Scan.char_reader(doc.text))
+      resources.check_thy_reader("", node_name, Scan.char_reader(content.text))
 
 
   /* perspective */
@@ -69,21 +77,21 @@
 
   def get_blob: Option[Document.Blob] =
     if (is_theory) None
-    else Some((Document.Blob(doc.bytes, doc.chunk, pending_edits.nonEmpty)))
+    else Some((Document.Blob(content.bytes, content.chunk, pending_edits.nonEmpty)))
 
 
   /* edits */
 
   def update_text(text: String): Option[Document_Model] =
   {
-    val old_text = doc.text
+    val old_text = content.text
     val new_text = Line.normalize(text)
     Text.Edit.replace(0, old_text, new_text) match {
       case Nil => None
       case edits =>
-        val doc1 = Line.Document(new_text, doc.text_length)
+        val content1 = Document_Model.Content(Line.Document(new_text, content.doc.text_length))
         val pending_edits1 = pending_edits ::: edits
-        Some(copy(doc = doc1, pending_edits = pending_edits1))
+        Some(copy(content = content1, pending_edits = pending_edits1))
     }
   }
 

--- a/src/Tools/VSCode/src/server.scala	Sun Jan 08 11:41:18 2017 +0100
+++ b/src/Tools/VSCode/src/server.scala	Sun Jan 08 12:00:37 2017 +0100
@@ -104,7 +104,7 @@
     for {
       model <- resources.get_model(new JFile(node_pos.name))
       rendering = model.rendering()
-      offset <- model.doc.offset(node_pos.pos)
+      offset <- model.content.doc.offset(node_pos.pos)
     } yield (rendering, offset)
 
 
@@ -286,7 +286,7 @@
         (rendering, offset) <- rendering_offset(node_pos)
         info <- rendering.tooltips(Text.Range(offset, offset + 1))
       } yield {
-        val doc = rendering.model.doc
+        val doc = rendering.model.content.doc
         val range = doc.range(info.range)
         val contents =
           info.info.map(tree => Pretty.string_of(List(tree), margin = rendering.tooltip_margin))
@@ -314,7 +314,7 @@
     val result =
       (for ((rendering, offset) <- rendering_offset(node_pos))
         yield {
-          val doc = rendering.model.doc
+          val doc = rendering.model.content.doc
           rendering.caret_focus_ranges(Text.Range(offset, offset + 1), doc.text_range)
             .map(r => Protocol.DocumentHighlight.text(doc.range(r)))
         }) getOrElse Nil

--- a/src/Tools/VSCode/src/vscode_rendering.scala	Sun Jan 08 11:41:18 2017 +0100
+++ b/src/Tools/VSCode/src/vscode_rendering.scala	Sun Jan 08 12:00:37 2017 +0100
@@ -47,7 +47,7 @@
 
   def diagnostics: List[Text.Info[Command.Results]] =
     snapshot.cumulate[Command.Results](
-      model.doc.text_range, Command.Results.empty, VSCode_Rendering.diagnostics_elements, _ =>
+      model.content.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))
@@ -61,7 +61,7 @@
   {
     (for {
       Text.Info(text_range, res) <- results.iterator
-      range = model.doc.range(text_range)
+      range = model.content.doc.range(text_range)
       (_, XML.Elem(Markup(name, _), body)) <- res.iterator
     } yield {
       val message = Pretty.string_of(body, margin = diagnostics_margin)

--- a/src/Tools/VSCode/src/vscode_resources.scala	Sun Jan 08 11:41:18 2017 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Sun Jan 08 12:00:37 2017 +0100
@@ -71,7 +71,7 @@
   {
     val file = node_file(name)
     get_model(file) match {
-      case Some(model) => f(Scan.char_reader(model.doc.text))
+      case Some(model) => f(Scan.char_reader(model.content.text))
       case None if file.isFile =>
         val reader = Scan.byte_reader(file)
         try { f(reader) } finally { reader.close }
@@ -138,7 +138,7 @@
 
   def get_file_content(file: JFile): Option[String] =
     get_model(file) match {
-      case Some(model) => Some(model.doc.text)
+      case Some(model) => Some(model.content.text)
       case None => read_file_content(file)
     }