src/Tools/VSCode/src/vscode_resources.scala
changeset 64707 7157685b71e3
parent 64706 3ebf9f8299df
child 64708 dd7f1a7e03f4
--- a/src/Tools/VSCode/src/vscode_resources.scala	Fri Dec 30 10:26:10 2016 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Fri Dec 30 11:46:34 2016 +0100
@@ -79,11 +79,12 @@
           (for {
             node_name <- st.pending_input.iterator
             model <- st.models.get(node_name.node)
-            if model.changed } yield model).toList
-        val edits = for { model <- changed; edit <- model.node_edits } yield edit
-        session.update(Document.Blobs.empty, edits)
+            res <- model.flush_edits
+          } yield res).toList
+
+        session.update(Document.Blobs.empty, changed.flatMap(_._1))
         st.copy(
-          models = (st.models /: changed) { case (ms, m) => ms + (m.uri -> m.unchanged) },
+          models = (st.models /: changed) { case (ms, (_, m)) => ms + (m.uri -> m) },
           pending_input = Set.empty)
       })
   }