# 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))(_ + _))) })