manage document blobs as well;

--- a/src/Pure/PIDE/line.scala	Thu Jan 05 12:23:25 2017 +0100
+++ b/src/Pure/PIDE/line.scala	Thu Jan 05 15:15:51 2017 +0100
@@ -136,6 +136,12 @@
       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))
+    }
   }
 
 

--- a/src/Tools/VSCode/src/document_model.scala	Thu Jan 05 12:23:25 2017 +0100
+++ b/src/Tools/VSCode/src/document_model.scala	Thu Jan 05 15:15:51 2017 +0100
@@ -45,6 +45,8 @@
 
   def external(b: Boolean): Document_Model = copy(external_file = b)
 
+  def node_visible: Boolean = !external_file
+
 
   /* header */
 
@@ -60,13 +62,32 @@
 
   /* perspective */
 
-  def node_visible: Boolean = !external_file
+  def node_perspective(doc_blobs: Document.Blobs): (Boolean, Document.Node.Perspective_Text) =
+  {
+    if (is_theory) {
+      val snapshot = this.snapshot()
+
+      val text_perspective =
+        if (node_visible || snapshot.commands_loading_ranges(resources.visible_node(_)).nonEmpty)
+          Text.Perspective.full
+        else Text.Perspective.empty
 
-  def text_perspective: Text.Perspective =
-    if (node_visible) Text.Perspective.full else Text.Perspective.empty
+      (snapshot.node.load_commands_changed(doc_blobs),
+        Document.Node.Perspective(node_required, text_perspective, Document.Node.Overlays.empty))
+    }
+    else (false, Document.Node.no_perspective_text)
+  }
+
 
-  def node_perspective: Document.Node.Perspective_Text =
-    Document.Node.Perspective(node_required, text_perspective, Document.Node.Overlays.empty)
+  /* blob */
+
+  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)))
+    }
 
 
   /* edits */
@@ -84,17 +105,20 @@
     }
   }
 
-  def flush_edits: Option[(List[Document.Edit_Text], Document_Model)] =
+  def flush_edits(doc_blobs: Document.Blobs): Option[(List[Document.Edit_Text], Document_Model)] =
   {
-    val perspective = node_perspective
-    if (pending_edits.nonEmpty || last_perspective != perspective) {
-      val text_edits = pending_edits.toList
-      val edits =
-        session.header_edit(node_name, node_header) ::
-        (if (text_edits.isEmpty) Nil
-         else List[Document.Edit_Text](node_name -> Document.Node.Edits(text_edits))) :::
-        (if (last_perspective == perspective) Nil
-         else List[Document.Edit_Text](node_name -> perspective))
+    val (reparse, perspective) = node_perspective(doc_blobs)
+    if (reparse || pending_edits.nonEmpty || last_perspective != perspective) {
+      val edits: List[Document.Edit_Text] =
+        get_blob match {
+          case None =>
+            List(session.header_edit(node_name, node_header),
+              node_name -> Document.Node.Edits(pending_edits.toList),
+              node_name -> perspective)
+          case Some(blob) =>
+            List(node_name -> Document.Node.Blob(blob),
+              node_name -> Document.Node.Edits(pending_edits.toList))
+        }
       Some((edits, copy(pending_edits = Vector.empty, last_perspective = perspective)))
     }
     else None

--- a/src/Tools/VSCode/src/server.scala	Thu Jan 05 12:23:25 2017 +0100
+++ b/src/Tools/VSCode/src/server.scala	Thu Jan 05 15:15:51 2017 +0100
@@ -110,13 +110,16 @@
 
   /* input from client or file-system */
 
-  private val delay_input =
+  private val delay_input: Standard_Thread.Delay =
     Standard_Thread.delay_last(options.seconds("vscode_input_delay"))
     { resources.flush_input(session) }
 
-  private val delay_load =
-    Standard_Thread.delay_last(options.seconds("vscode_load_delay"))
-    { if (resources.resolve_dependencies(session, watcher)) delay_input.invoke() }
+  private val delay_load: Standard_Thread.Delay =
+    Standard_Thread.delay_last(options.seconds("vscode_load_delay")) {
+      val (invoke_input, invoke_load) = resources.resolve_dependencies(session, watcher)
+      if (invoke_input) delay_input.invoke()
+      if (invoke_load) delay_load.invoke
+    }
 
   private val watcher =
     File_Watcher(sync_documents(_), options.seconds("vscode_load_delay"))
@@ -201,7 +204,8 @@
           new VSCode_Resources(options, text_length, content.loaded_theories,
               content.known_theories, content.syntax, log) {
             override def commit(change: Session.Change): Unit =
-              if (change.deps_changed) delay_load.invoke()
+              if (change.deps_changed || undefined_blobs(change.version.nodes).nonEmpty)
+                delay_load.invoke()
           }
 
         Some(new Session(resources) {

--- a/src/Tools/VSCode/src/vscode_resources.scala	Thu Jan 05 12:23:25 2017 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Thu Jan 05 15:15:51 2017 +0100
@@ -22,6 +22,14 @@
     models: Map[JFile, Document_Model] = Map.empty,
     pending_input: Set[JFile] = Set.empty,
     pending_output: Set[JFile] = Set.empty)
+  {
+    lazy val document_blobs: Document.Blobs =
+      Document.Blobs(
+        (for {
+          (_, model) <- models.iterator
+          blob <- model.get_blob
+        } yield (model.node_name -> blob)).toMap)
+  }
 }
 
 class VSCode_Resources(
@@ -79,6 +87,12 @@
   def get_model(file: JFile): Option[Document_Model] = state.value.models.get(file)
   def get_model(name: Document.Node.Name): Option[Document_Model] = get_model(node_file(name))
 
+  def visible_node(name: Document.Node.Name): Boolean =
+    get_model(name) match {
+      case Some(model) => model.node_visible
+      case None => false
+    }
+
   def update_model(session: Session, file: JFile, text: String)
   {
     state.change(st =>
@@ -134,33 +148,55 @@
 
   val thy_info = new Thy_Info(this)
 
-  def resolve_dependencies(session: Session, watcher: File_Watcher): Boolean =
+  def resolve_dependencies(session: Session, watcher: File_Watcher): (Boolean, Boolean) =
   {
     state.change_result(st =>
       {
+        /* theory files */
+
         val thys =
           (for ((_, model) <- st.models.iterator if model.is_theory)
            yield (model.node_name, Position.none)).toList
 
+        val thy_files = thy_info.dependencies("", thys).deps.map(_.name)
+
+
+        /* auxiliary files */
+
+        val stable_tip_version =
+          if (st.models.forall({ case (_, model) => model.pending_edits.isEmpty }))
+            session.current_state().stable_tip_version
+          else None
+
+        val aux_files =
+          stable_tip_version match {
+            case Some(version) => undefined_blobs(version.nodes)
+            case None => Nil
+          }
+
+
+        /* loaded models */
+
         val loaded_models =
           (for {
-            dep <- thy_info.dependencies("", thys).deps.iterator
-            file = node_file(dep.name)
+            node_name <- thy_files.iterator ++ aux_files.iterator
+            file = node_file(node_name)
             if !st.models.isDefinedAt(file)
             text <- { watcher.register_parent(file); try_read(file) }
           }
           yield {
-            val model = Document_Model.init(session, node_name(file))
+            val model = Document_Model.init(session, node_name)
             val model1 = (model.update_text(text) getOrElse model).external(true)
             (file, model1)
           }).toList
 
-        if (loaded_models.isEmpty) (false, st)
-        else
-          (true,
-            st.copy(
-              models = st.models ++ loaded_models,
-              pending_input = st.pending_input ++ loaded_models.iterator.map(_._1)))
+        val invoke_input = loaded_models.nonEmpty
+        val invoke_load = stable_tip_version.isEmpty
+
+        ((invoke_input, invoke_load),
+          st.copy(
+            models = st.models ++ loaded_models,
+            pending_input = st.pending_input ++ loaded_models.iterator.map(_._1)))
       })
   }
 
@@ -175,10 +211,10 @@
           (for {
             file <- st.pending_input.iterator
             model <- st.models.get(file)
-            (edits, model1) <- model.flush_edits
+            (edits, model1) <- model.flush_edits(st.document_blobs)
           } yield (edits, (file, model1))).toList
 
-        session.update(Document.Blobs.empty, changed_models.flatMap(_._1))
+        session.update(st.document_blobs, changed_models.flatMap(_._1))
         st.copy(
           models = (st.models /: changed_models.iterator.map(_._2))(_ + _),
           pending_input = Set.empty)