# HG changeset patch
# User wenzelm
# Date 1483190827 -3600
# Node ID 4b9c96c3850b299ed8391bb039a2c6bbefebdb1d
# Parent  8cc2d7c4ada1d3d108e3c44ac2cae3e0e59e6c3e
proper state update;

diff -r 8cc2d7c4ada1 -r 4b9c96c3850b src/Tools/VSCode/src/vscode_resources.scala
--- a/src/Tools/VSCode/src/vscode_resources.scala	Sat Dec 31 14:20:50 2016 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Sat Dec 31 14:27:07 2016 +0100
@@ -97,9 +97,12 @@
             (uri, model) <- st.models.iterator
             if changed_files(model.file)
             model1 <- model.update_file
-          } yield (uri, model)).toList
+          } yield (uri, model1)).toList
         if (changed_models.isEmpty) (false, st)
-        else (true, st.copy(models = (st.models /: changed_models)(_ + _)))
+        else (true,
+          st.copy(
+            models = (st.models /: changed_models)(_ + _),
+            pending_input = (st.pending_input /: changed_models.iterator.map(_._1))(_ + _)))
       })