--- a/src/Tools/VSCode/src/vscode_resources.scala Wed Mar 03 22:48:46 2021 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala Thu Mar 04 15:41:46 2021 +0100
@@ -28,8 +28,8 @@
def update_models(changed: Iterable[(JFile, VSCode_Model)]): State =
copy(
models = models ++ changed,
- pending_input = (pending_input /: changed) { case (set, (file, _)) => set + file },
- pending_output = (pending_output /: changed) { case (set, (file, _)) => set + file })
+ pending_input = changed.foldLeft(pending_input) { case (set, (file, _)) => set + file },
+ pending_output = changed.foldLeft(pending_output) { case (set, (file, _)) => set + file })
def update_caret(new_caret: Option[(JFile, Line.Position)]): State =
if (caret == new_caret) this