src/Tools/VSCode/src/vscode_resources.scala
changeset 64710 72ca4e5f976e
parent 64709 5e6566ab78bf
child 64716 473793d52d97
--- a/src/Tools/VSCode/src/vscode_resources.scala	Fri Dec 30 17:45:00 2016 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Fri Dec 30 20:36:13 2016 +0100
@@ -64,13 +64,35 @@
   {
     state.change(st =>
       {
-        val model = st.models.getOrElse(uri, Document_Model.init(session, uri)).update_text(text)
+        val model = st.models.getOrElse(uri, Document_Model.init(session, uri))
+        val model1 = (model.update_text(text) getOrElse model).copy(external = false)
         st.copy(
-          models = st.models + (uri -> model),
+          models = st.models + (uri -> model1),
           pending_input = st.pending_input + uri)
       })
   }
 
+  def close_model(uri: String): Option[Document_Model] =
+    state.change_result(st =>
+      st.models.get(uri) match {
+        case None => (None, st)
+        case Some(model) =>
+          (Some(model), st.copy(models = st.models + (uri -> model.copy(external = true))))
+      })
+
+  def sync_external(changed_files: Set[JFile]): Boolean =
+    state.change_result(st =>
+      {
+        val changed =
+          (for {
+            (uri, model) <- st.models.iterator
+            if changed_files(model.file)
+            model1 <- model.update_file
+          } yield (uri, model)).toList
+        if (changed.isEmpty) (false, st)
+        else (true, st.copy(models = (st.models /: changed)(_ + _)))
+      })
+
 
   /* pending input */