--- 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)
}
)