src/Pure/PIDE/headless.scala

--- a/src/Pure/PIDE/headless.scala	Wed Mar 03 22:48:46 2021 +0100
+++ b/src/Pure/PIDE/headless.scala	Thu Mar 04 15:41:46 2021 +0100
@@ -154,7 +154,8 @@
           if (add.isEmpty) front
           else {
             val preds = add.map(dep_graph.imm_preds)
-            val base1 = (preds.head /: preds.tail)(_ ++ _).toList.filter(already_committed.keySet)
+            val base1 =
+              preds.tail.foldLeft(preds.head)(_ ++ _).toList.filter(already_committed.keySet)
             frontier(base1, front ++ add)
           }
         }
@@ -182,21 +183,21 @@
           commit match {
             case None => already_committed
             case Some(commit_fn) =>
-              (already_committed /: dep_graph.topological_order)(
-                { case (committed, name) =>
-                    def parents_committed: Boolean =
-                      version.nodes(name).header.imports.forall(parent =>
-                        loaded_theory(parent) || committed.isDefinedAt(parent))
-                    if (!committed.isDefinedAt(name) && parents_committed &&
-                        state.node_consolidated(version, name))
-                    {
-                      val snapshot = stable_snapshot(state, version, name)
-                      val status = Document_Status.Node_Status.make(state, version, name)
-                      commit_fn(snapshot, status)
-                      committed + (name -> status)
-                    }
-                    else committed
-                })
+              dep_graph.topological_order.foldLeft(already_committed) {
+                case (committed, name) =>
+                  def parents_committed: Boolean =
+                    version.nodes(name).header.imports.forall(parent =>
+                      loaded_theory(parent) || committed.isDefinedAt(parent))
+                  if (!committed.isDefinedAt(name) && parents_committed &&
+                      state.node_consolidated(version, name))
+                  {
+                    val snapshot = stable_snapshot(state, version, name)
+                    val status = Document_Status.Node_Status.make(state, version, name)
+                    commit_fn(snapshot, status)
+                    committed + (name -> status)
+                  }
+                  else committed
+              }
           }
 
         def finished_theory(name: Document.Node.Name): Boolean =
@@ -472,8 +473,8 @@
               case None => Some(name -> new_blob)
             }
           })
-        val blobs1 = (blobs /: new_blobs)(_ + _)
-        val blobs2 = (blobs /: new_blobs)({ case (map, (a, b)) => map + (a -> b.unchanged) })
+        val blobs1 = new_blobs.foldLeft(blobs)(_ + _)
+        val blobs2 = new_blobs.foldLeft(blobs) { case (map, (a, b)) => map + (a -> b.unchanged) }
         (Document.Blobs(blobs1), copy(blobs = blobs2))
       }
 
@@ -501,19 +502,20 @@
       def is_required(name: Document.Node.Name): Boolean = required.isDefinedAt(name)
 
       def insert_required(id: UUID.T, names: List[Document.Node.Name]): State =
-        copy(required = (required /: names)(_.insert(_, id)))
+        copy(required = names.foldLeft(required)(_.insert(_, id)))
 
       def remove_required(id: UUID.T, names: List[Document.Node.Name]): State =
-        copy(required = (required /: names)(_.remove(_, id)))
+        copy(required = names.foldLeft(required)(_.remove(_, id)))
 
       def update_theories(update: List[(Document.Node.Name, Theory)]): State =
         copy(theories =
-          (theories /: update)({ case (thys, (name, thy)) =>
-            thys.get(name) match {
-              case Some(thy1) if thy1 == thy => thys
-              case _ => thys + (name -> thy)
-            }
-          }))
+          update.foldLeft(theories) {
+            case (thys, (name, thy)) =>
+              thys.get(name) match {
+                case Some(thy1) if thy1 == thy => thys
+                case _ => thys + (name -> thy)
+              }
+          })
 
       def remove_theories(remove: List[Document.Node.Name]): State =
       {