# HG changeset patch
# User wenzelm
# Date 1488718451 -3600
# Node ID b3904f683ef5f66d23df7604861b68156e814d8d
# Parent  3224a6f7bd6b0c4008f3b13d302cd7803ab9c17e
tuned;

diff -r 3224a6f7bd6b -r b3904f683ef5 src/Tools/VSCode/src/vscode_resources.scala
--- a/src/Tools/VSCode/src/vscode_resources.scala	Sun Mar 05 13:34:35 2017 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Sun Mar 05 13:54:11 2017 +0100
@@ -219,7 +219,7 @@
 
         session.update(st.document_blobs, changed_models.flatMap(_._1))
         st.copy(
-          models = (st.models /: changed_models.iterator.map(_._2))(_ + _),
+          models = st.models ++ changed_models.iterator.map(_._2),
           pending_input = Set.empty)
       })
   }
@@ -252,7 +252,7 @@
             (file, model1)
           }
         st.copy(
-          models = (st.models /: changed_iterator)(_ + _),
+          models = st.models ++ changed_iterator,
           pending_output = Set.empty)
       }
     )