src/Tools/VSCode/src/vscode_resources.scala

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