# HG changeset patch
# User wenzelm
# Date 1488719638 -3600
# Node ID 200b787ceb51a12827d15f691c8c7dfbcc99531e
# Parent  6058e7d31fe6b317b322a3b07769eab74548e08e
potentially redundant pending_output, for the sake of uniformity and reactivity;

diff -r 6058e7d31fe6 -r 200b787ceb51 src/Tools/VSCode/src/vscode_resources.scala
--- a/src/Tools/VSCode/src/vscode_resources.scala	Sun Mar 05 14:11:24 2017 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Sun Mar 05 14:13:58 2017 +0100
@@ -120,11 +120,7 @@
       {
         val model = st.models.getOrElse(file, Document_Model.init(session, node_name(file)))
         val model1 = (model.update_text(text) getOrElse model).external(false)
-        st.copy(
-          models = st.models + (file -> model1),
-          pending_input = st.pending_input + file,
-          pending_output = st.pending_output ++
-            (if (model.node_visible == model1.node_visible) None else Some(file)))
+        st.update_models(Some(file -> model1))
       })
   }