src/Tools/jEdit/src/document_model.scala

--- a/src/Tools/jEdit/src/document_model.scala	Wed Mar 03 22:31:11 2021 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Wed Mar 03 22:48:46 2021 +0100
@@ -127,7 +127,7 @@
             (node_name, model.copy(content = content, pending_edits = model.pending_edits ::: edits))
           }).toList
         if (changed_models.isEmpty) (false, st)
-        else (true, st.copy(models = (st.models /: changed_models)(_ + _)))
+        else (true, st.copy(models = changed_models.foldLeft(st.models)(_ + _)))
       })
   }
 
@@ -178,7 +178,9 @@
   {
     GUI_Thread.require {}
     state.change(st =>
-      (st /: files) { case (st1, (node_name, text)) => st1.provide_file(session, node_name, text) })
+      files.foldLeft(st) {
+        case (st1, (node_name, text)) => st1.provide_file(session, node_name, text)
+      })
   }