tuned --- fewer warnings;
authorwenzelm
Thu, 04 Mar 2021 15:41:46 +0100
changeset 73606 d8a0e996614b
parent 73605 78aa7846e91f
child 73607 4123fca23296
tuned --- fewer warnings;
src/Pure/Admin/afp.scala
src/Pure/Admin/build_csdp.scala
src/Pure/Admin/build_history.scala
src/Pure/Admin/build_status.scala
src/Pure/Admin/ci_profile.scala
src/Pure/Admin/isabelle_cronjob.scala
src/Pure/General/completion.scala
src/Pure/General/file_watcher.scala
src/Pure/General/graph.scala
src/Pure/General/graph_display.scala
src/Pure/General/linear_set.scala
src/Pure/General/mercurial.scala
src/Pure/General/multi_map.scala
src/Pure/General/path.scala
src/Pure/General/pretty.scala
src/Pure/General/scan.scala
src/Pure/General/symbol.scala
src/Pure/Isar/document_structure.scala
src/Pure/Isar/keyword.scala
src/Pure/Isar/line_structure.scala
src/Pure/Isar/outer_syntax.scala
src/Pure/ML/ml_statistics.scala
src/Pure/PIDE/command.scala
src/Pure/PIDE/command_span.scala
src/Pure/PIDE/document.scala
src/Pure/PIDE/document_status.scala
src/Pure/PIDE/headless.scala
src/Pure/PIDE/line.scala
src/Pure/PIDE/markup_tree.scala
src/Pure/PIDE/protocol_handlers.scala
src/Pure/PIDE/prover.scala
src/Pure/PIDE/rendering.scala
src/Pure/PIDE/resources.scala
src/Pure/PIDE/xml.scala
src/Pure/System/getopts.scala
src/Pure/System/options.scala
src/Pure/Thy/bibtex.scala
src/Pure/Thy/export_theory.scala
src/Pure/Thy/file_format.scala
src/Pure/Thy/latex.scala
src/Pure/Thy/sessions.scala
src/Pure/Thy/thy_header.scala
src/Pure/Thy/thy_syntax.scala
src/Pure/Tools/build.scala
src/Pure/Tools/dump.scala
src/Pure/Tools/scala_project.scala
src/Pure/Tools/server.scala
src/Tools/Graphview/layout.scala
src/Tools/Graphview/metrics.scala
src/Tools/Graphview/model.scala
src/Tools/Graphview/mutator.scala
src/Tools/Graphview/shapes.scala
src/Tools/VSCode/src/preview_panel.scala
src/Tools/VSCode/src/vscode_rendering.scala
src/Tools/VSCode/src/vscode_resources.scala
src/Tools/jEdit/src/isabelle_sidekick.scala
src/Tools/jEdit/src/pretty_tooltip.scala
src/Tools/jEdit/src/text_structure.scala
src/Tools/jEdit/src/theories_dockable.scala
src/Tools/jEdit/src/timing_dockable.scala
--- a/src/Pure/Admin/afp.scala	Wed Mar 03 22:48:46 2021 +0100
+++ b/src/Pure/Admin/afp.scala	Thu Mar 04 15:41:46 2021 +0100
@@ -136,7 +136,7 @@
       }
 
     val entries_map =
-      (SortedMap.empty[String, AFP.Entry] /: entries)({ case (m, e) => m + (e.name -> e) })
+      entries.foldLeft(SortedMap.empty[String, AFP.Entry]) { case (m, e) => m + (e.name -> e) }
 
     val extra_metadata =
       (for ((name, _) <- entry_metadata.iterator if !entries_map.isDefinedAt(name)) yield name).
@@ -153,8 +153,9 @@
   /* sessions */
 
   val sessions_map: SortedMap[String, AFP.Entry] =
-    (SortedMap.empty[String, AFP.Entry] /: entries)(
-      { case (m1, e) => (m1 /: e.sessions)({ case (m2, s) => m2 + (s -> e) }) })
+    entries.foldLeft(SortedMap.empty[String, AFP.Entry]) {
+      case (m1, e) => e.sessions.foldLeft(m1) { case (m2, s) => m2 + (s -> e) }
+    }
 
   val sessions: List[String] = entries.flatMap(_.sessions)
 
@@ -171,22 +172,25 @@
   lazy val entries_graph: Graph[String, Unit] =
   {
     val session_entries =
-      (Map.empty[String, String] /: entries) {
-        case (m1, e) => (m1 /: e.sessions) { case (m2, s) => m2 + (s -> e.name) }
+      entries.foldLeft(Map.empty[String, String]) {
+        case (m1, e) => e.sessions.foldLeft(m1) { case (m2, s) => m2 + (s -> e.name) }
       }
-    (Graph.empty[String, Unit] /: entries) { case (g, entry) =>
-      val e1 = entry.name
-      (g.default_node(e1, ()) /: sessions_deps(entry)) { case (g1, s) =>
-        (g1 /: session_entries.get(s).filterNot(_ == e1)) { case (g2, e2) =>
-          try { g2.default_node(e2, ()).add_edge_acyclic(e2, e1) }
-          catch {
-            case exn: Graph.Cycles[_] =>
-              error(cat_lines(exn.cycles.map(cycle =>
-                "Cyclic dependency of " + cycle.map(c => quote(c.toString)).mkString(" via ") +
-                " due to session " + quote(s))))
-          }
+    entries.foldLeft(Graph.empty[String, Unit]) {
+      case (g, entry) =>
+        val e1 = entry.name
+        sessions_deps(entry).foldLeft(g.default_node(e1, ())) {
+          case (g1, s) =>
+            session_entries.get(s).filterNot(_ == e1).foldLeft(g1) {
+              case (g2, e2) =>
+                try { g2.default_node(e2, ()).add_edge_acyclic(e2, e1) }
+                catch {
+                  case exn: Graph.Cycles[_] =>
+                    error(cat_lines(exn.cycles.map(cycle =>
+                      "Cyclic dependency of " + cycle.map(c => quote(c.toString)).mkString(" via ") +
+                      " due to session " + quote(s))))
+                }
+            }
         }
-      }
     }
   }
 
--- a/src/Pure/Admin/build_csdp.scala	Wed Mar 03 22:48:46 2021 +0100
+++ b/src/Pure/Admin/build_csdp.scala	Thu Mar 04 15:41:46 2021 +0100
@@ -31,7 +31,7 @@
       def change_line(line: String, entry: (String, String)): String =
         line.replaceAll(entry._1 + "=.*", entry._1 + "=" + entry._2)
       File.change(path, s =>
-        split_lines(s).map(line => (line /: changed)(change_line)).mkString("\n"))
+        split_lines(s).map(line => changed.foldLeft(line)(change_line)).mkString("\n"))
     }
   }
 
--- a/src/Pure/Admin/build_history.scala	Wed Mar 03 22:48:46 2021 +0100
+++ b/src/Pure/Admin/build_history.scala	Thu Mar 04 15:41:46 2021 +0100
@@ -519,7 +519,7 @@
           cat_lines(for ((_, log_path) <- results) yield log_path.implode))
       }
 
-      val rc = (0 /: results) { case (rc, (res, _)) => rc max res.rc }
+      val rc = results.foldLeft(0) { case (rc, (res, _)) => rc max res.rc }
       if (rc != 0 && exit_code) sys.exit(rc)
     }
   }
--- a/src/Pure/Admin/build_status.scala	Wed Mar 03 22:48:46 2021 +0100
+++ b/src/Pure/Admin/build_status.scala	Thu Mar 04 15:41:46 2021 +0100
@@ -429,11 +429,13 @@
                       entry.stored_heap.toString).mkString(" "))))
 
               val max_time =
-                ((0.0 /: session.finished_entries){ case (m, entry) =>
-                  m.max(entry.timing.elapsed.minutes).
-                    max(entry.timing.resources.minutes).
-                    max(entry.ml_timing.elapsed.minutes).
-                    max(entry.ml_timing.resources.minutes) } max 0.1) * 1.1
+                (session.finished_entries.foldLeft(0.0) {
+                  case (m, entry) =>
+                    m.max(entry.timing.elapsed.minutes).
+                      max(entry.timing.resources.minutes).
+                      max(entry.ml_timing.elapsed.minutes).
+                      max(entry.ml_timing.resources.minutes)
+                } max 0.1) * 1.1
               val timing_range = "[0:" + max_time + "]"
 
               def gnuplot(plot_name: String, plots: List[String], range: String): Image =
--- a/src/Pure/Admin/ci_profile.scala	Wed Mar 03 22:48:46 2021 +0100
+++ b/src/Pure/Admin/ci_profile.scala	Thu Mar 04 15:41:46 2021 +0100
@@ -56,7 +56,7 @@
       case session if group.forall(results.info(session).groups.contains(_)) =>
         results(session).timing
     }
-    (Timing.zero /: timings)(_ + _)
+    timings.foldLeft(Timing.zero)(_ + _)
   }
 
   private def with_documents(options: Options): Options =
--- a/src/Pure/Admin/isabelle_cronjob.scala	Wed Mar 03 22:48:46 2021 +0100
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Thu Mar 04 15:41:46 2021 +0100
@@ -183,9 +183,9 @@
 
           if (historic || items.exists(_.known_versions(rev, afp_rev))) {
             val longest_run =
-              (List.empty[Item] /: runs)({ case (item1, item2) =>
-                if (item1.length >= item2.length) item1 else item2
-              })
+              runs.foldLeft(List.empty[Item]) {
+                case (item1, item2) => if (item1.length >= item2.length) item1 else item2
+              }
             if (longest_run.isEmpty) None
             else Some(longest_run(longest_run.length / 2).versions)
           }
--- a/src/Pure/General/completion.scala	Wed Mar 03 22:48:46 2021 +0100
+++ b/src/Pure/General/completion.scala	Thu Mar 04 15:41:46 2021 +0100
@@ -32,7 +32,7 @@
   {
     def empty(range: Text.Range): Result = Result(range, "", false, Nil)
     def merge(history: History, results: Option[Result]*): Option[Result] =
-      ((None: Option[Result]) /: results)({
+      results.foldLeft(None: Option[Result]) {
         case (result1, None) => result1
         case (None, result2) => result2
         case (result1 @ Some(res1), Some(res2)) =>
@@ -41,7 +41,7 @@
             val items = (res1.items ::: res2.items).sorted(history.ordering)
             Some(Result(res1.range, res1.original, false, items))
           }
-      })
+      }
   }
 
   sealed case class Result(
@@ -78,7 +78,7 @@
           }
         }
         else Nil
-      (empty /: content)(_ + _)
+      content.foldLeft(empty)(_ + _)
     }
   }
 
@@ -356,7 +356,7 @@
 
   def add_keywords(names: List[String]): Completion =
   {
-    val keywords1 = (keywords /: names) { case (ks, k) => if (ks(k)) ks else ks + k }
+    val keywords1 = names.foldLeft(keywords) { case (ks, k) => if (ks(k)) ks else ks + k }
     if (keywords eq keywords1) this
     else new Completion(keywords1, words_lex, words_map, abbrevs_lex, abbrevs_map)
   }
@@ -386,7 +386,7 @@
   }
 
   def add_abbrevs(abbrevs: List[(String, String)]): Completion =
-    (this /: abbrevs)(_.add_abbrev(_))
+    abbrevs.foldLeft(this)(_.add_abbrev(_))
 
   private def add_abbrev(abbrev: (String, String)): Completion =
     abbrev match {
--- a/src/Pure/General/file_watcher.scala	Wed Mar 03 22:48:46 2021 +0100
+++ b/src/Pure/General/file_watcher.scala	Thu Mar 04 15:41:46 2021 +0100
@@ -105,7 +105,7 @@
                         key.pollEvents.asInstanceOf[java.util.List[WatchEvent[JPath]]].asScala
                       val remove = if (key.reset) None else Some(dir)
                       val changed =
-                        (Set.empty[JFile] /: events.iterator) {
+                        events.iterator.foldLeft(Set.empty[JFile]) {
                           case (set, event) => set + dir.toPath.resolve(event.context).toFile
                         }
                       (remove, changed)
--- a/src/Pure/General/graph.scala	Wed Mar 03 22:48:46 2021 +0100
+++ b/src/Pure/General/graph.scala	Thu Mar 04 15:41:46 2021 +0100
@@ -33,10 +33,16 @@
     symmetric: Boolean = false)(implicit ord: Ordering[Key]): Graph[Key, A] =
   {
     val graph1 =
-      (empty[Key, A](ord) /: entries) { case (graph, ((x, info), _)) => graph.new_node(x, info) }
+      entries.foldLeft(empty[Key, A](ord)) {
+        case (graph, ((x, info), _)) => graph.new_node(x, info)
+      }
     val graph2 =
-      (graph1 /: entries) { case (graph, ((x, _), ys)) =>
-        (graph /: ys)({ case (g, y) => if (symmetric) g.add_edge(y, x) else g.add_edge(x, y) }) }
+      entries.foldLeft(graph1) {
+        case (graph, ((x, _), ys)) =>
+          ys.foldLeft(graph) {
+            case (g, y) => if (symmetric) g.add_edge(y, x) else g.add_edge(x, y)
+          }
+      }
     graph2
   }
 
@@ -119,8 +125,8 @@
   {
     def reach(length: Long)(rs: Map[Key, Long], x: Key): Map[Key, Long] =
       if (rs.get(x) match { case Some(n) => n >= length case None => false }) rs
-      else ((rs + (x -> length)) /: next(x))(reach(length + count(x)))
-    (Map.empty[Key, Long] /: xs)(reach(0))
+      else next(x).foldLeft(rs + (x -> length))(reach(length + count(x)))
+    xs.foldLeft(Map.empty[Key, Long])(reach(0))
   }
   def node_height(count: Key => Long): Map[Key, Long] =
     reachable_length(count, imm_preds, maximals)
@@ -138,7 +144,7 @@
     {
       val (n, rs) = res
       if (rs.contains(x)) res
-      else ((n + count(x), rs + x) /: next(x))(reach)
+      else next(x).foldLeft((n + count(x), rs + x))(reach)
     }
 
     @tailrec def reachs(size: Long, rs: Keys, rest: List[Key]): Keys =
@@ -162,7 +168,7 @@
       if (r_set(x)) reached
       else {
         val (rs1, r_set1) =
-          if (rev) ((rs, r_set + x) /: next(x))({ case (b, a) => reach(a, b) })
+          if (rev) next(x).foldLeft((rs, r_set + x)) { case (b, a) => reach(a, b) }
           else (next(x) :\ (rs, r_set + x))(reach)
         (x :: rs1, r_set1)
       }
@@ -173,7 +179,7 @@
       val (rs, r_set1) = reach(x, (Nil, r_set))
       (rs :: rss, r_set1)
     }
-    ((List.empty[List[Key]], empty_keys) /: xs)(reachs)
+    xs.foldLeft((List.empty[List[Key]], empty_keys))(reachs)
   }
 
   /*immediate*/
@@ -195,12 +201,14 @@
   /* minimal and maximal elements */
 
   def minimals: List[Key] =
-    (List.empty[Key] /: rep) {
-      case (ms, (m, (_, (preds, _)))) => if (preds.isEmpty) m :: ms else ms }
+    rep.foldLeft(List.empty[Key]) {
+      case (ms, (m, (_, (preds, _)))) => if (preds.isEmpty) m :: ms else ms
+    }
 
   def maximals: List[Key] =
-    (List.empty[Key] /: rep) {
-      case (ms, (m, (_, (_, succs)))) => if (succs.isEmpty) m :: ms else ms }
+    rep.foldLeft(List.empty[Key]) {
+      case (ms, (m, (_, (_, succs)))) => if (succs.isEmpty) m :: ms else ms
+    }
 
   def is_minimal(x: Key): Boolean = imm_preds(x).isEmpty
   def is_maximal(x: Key): Boolean = imm_succs(x).isEmpty
@@ -231,11 +239,11 @@
   {
     val (preds, succs) = get_entry(x)._2
     new Graph[Key, A](
-      (((rep - x) /: preds)(del_adjacent(false, x)) /: succs)(del_adjacent(true, x)))
+      succs.foldLeft(preds.foldLeft(rep - x)(del_adjacent(false, x)))(del_adjacent(true, x)))
   }
 
   def restrict(pred: Key => Boolean): Graph[Key, A] =
-    (this /: iterator){ case (graph, (x, _)) => if (!pred(x)) graph.del_node(x) else graph }
+    iterator.foldLeft(this) { case (graph, (x, _)) => if (!pred(x)) graph.del_node(x) else graph }
 
   def exclude(pred: Key => Boolean): Graph[Key, A] = restrict(name => !pred(name))
 
@@ -283,7 +291,7 @@
     val (_, x_set) = reachable(imm_succs, List(x))
     def paths(path: List[Key])(ps: List[List[Key]], z: Key): List[List[Key]] =
       if (x == z) (z :: path) :: ps
-      else (ps /: irreducible_preds(x_set, path, z))(paths(z :: path))
+      else irreducible_preds(x_set, path, z).foldLeft(ps)(paths(z :: path))
     if ((x == y) && !is_edge(x, x)) List(Nil) else paths(Nil)(Nil, y)
   }
 
@@ -298,7 +306,7 @@
     graph
   }
 
-  def transitive_closure: Graph[Key, A] = (this /: keys_iterator)(_.transitive_step(_))
+  def transitive_closure: Graph[Key, A] = keys_iterator.foldLeft(this)(_.transitive_step(_))
 
   def transitive_reduction_acyclic: Graph[Key, A] =
   {
@@ -328,7 +336,7 @@
     }
 
   def add_deps_acyclic(y: Key, xs: List[Key]): Graph[Key, A] =
-    (this /: xs)(_.add_edge_acyclic(_, y))
+    xs.foldLeft(this)(_.add_edge_acyclic(_, y))
 
   def topological_order: List[Key] = all_succs(minimals)
 }
--- a/src/Pure/General/graph_display.scala	Wed Mar 03 22:48:46 2021 +0100
+++ b/src/Pure/General/graph_display.scala	Thu Mar 04 15:41:46 2021 +0100
@@ -43,14 +43,15 @@
   def build_graph(entries: List[Entry]): Graph =
   {
     val node =
-      (Map.empty[String, Node] /: entries) {
+      entries.foldLeft(Map.empty[String, Node]) {
         case (m, ((ident, (name, _)), _)) => m + (ident -> Node(name, ident))
       }
-    (((empty_graph /: entries) {
+    entries.foldLeft(
+      entries.foldLeft(empty_graph) {
         case (g, ((ident, (_, content)), _)) => g.new_node(node(ident), content)
-      }) /: entries) {
+      }) {
         case (g1, ((ident, _), parents)) =>
-          (g1 /: parents) { case (g2, parent) => g2.add_edge(node(parent), node(ident)) }
+          parents.foldLeft(g1) { case (g2, parent) => g2.add_edge(node(parent), node(ident)) }
       }
   }
 
--- a/src/Pure/General/linear_set.scala	Wed Mar 03 22:48:46 2021 +0100
+++ b/src/Pure/General/linear_set.scala	Thu Mar 04 15:41:46 2021 +0100
@@ -18,7 +18,7 @@
   private val empty_val: Linear_Set[Nothing] = new Linear_Set[Nothing](None, None, Map(), Map())
   override def empty[A]: Linear_Set[A] = empty_val.asInstanceOf[Linear_Set[A]]
 
-  def from[A](entries: IterableOnce[A]): Linear_Set[A] = (empty[A] /: entries)(_.incl(_))
+  def from[A](entries: IterableOnce[A]): Linear_Set[A] = entries.foldLeft(empty[A])(_.incl(_))
 
   override def newBuilder[A]: mutable.Builder[A, Linear_Set[A]] = new Builder[A]
   private class Builder[A] extends mutable.Builder[A, Linear_Set[A]]
@@ -83,7 +83,7 @@
       }
 
   def append_after(hook: Option[A], elems: Iterable[A]): Linear_Set[A] =  // FIXME reverse fold
-    ((hook, this) /: elems) {
+    elems.foldLeft((hook, this)) {
       case ((last, set), elem) => (Some(elem), set.insert_after(last, elem))
     }._2
 
--- a/src/Pure/General/mercurial.scala	Wed Mar 03 22:48:46 2021 +0100
+++ b/src/Pure/General/mercurial.scala	Thu Mar 04 15:41:46 2021 +0100
@@ -144,11 +144,11 @@
       val Node = """^node: (\w{12}) (\w{12}) (\w{12})""".r
       val log_result =
         log(template = """node: {node|short} {p1node|short} {p2node|short}\n""")
-      (Graph.string[Unit] /: split_lines(log_result)) {
+      split_lines(log_result).foldLeft(Graph.string[Unit]) {
         case (graph, Node(x, y, z)) =>
           val deps = List(y, z).filterNot(s => s.forall(_ == '0'))
-          val graph1 = (graph /: (x :: deps))(_.default_node(_, ()))
-          (graph1 /: deps)({ case (g, dep) => g.add_edge(dep, x) })
+          val graph1 = (x :: deps).foldLeft(graph)(_.default_node(_, ()))
+          deps.foldLeft(graph1)({ case (g, dep) => g.add_edge(dep, x) })
         case (graph, _) => graph
       }
     }
--- a/src/Pure/General/multi_map.scala	Wed Mar 03 22:48:46 2021 +0100
+++ b/src/Pure/General/multi_map.scala	Thu Mar 04 15:41:46 2021 +0100
@@ -17,7 +17,7 @@
   def empty[A, B]: Multi_Map[A, B] = empty_val.asInstanceOf[Multi_Map[A, B]]
 
   def from[A, B](entries: IterableOnce[(A, B)]): Multi_Map[A, B] =
-    (empty[A, B] /: entries)({ case (m, (a, b)) => m.insert(a, b) })
+    entries.foldLeft(empty[A, B]) { case (m, (a, b)) => m.insert(a, b) }
 
   override def newBuilder[A, B]: mutable.Builder[(A, B), Multi_Map[A, B]] = new Builder[A, B]
   private class Builder[A, B] extends mutable.Builder[(A, B), Multi_Map[A, B]]
@@ -63,7 +63,7 @@
     if (this eq other) this
     else if (isEmpty) other
     else
-      (this.asInstanceOf[Multi_Map[A, B1]] /: other.rep.iterator) {
+      other.rep.iterator.foldLeft(this.asInstanceOf[Multi_Map[A, B1]]) {
         case (m1, (a, bs)) => (bs :\ m1) { case (b, m2) => m2.insert(a, b) }
       }
 
--- a/src/Pure/General/path.scala	Wed Mar 03 22:48:46 2021 +0100
+++ b/src/Pure/General/path.scala	Thu Mar 04 15:41:46 2021 +0100
@@ -146,10 +146,10 @@
   def check_case_insensitive(paths: List[Path]): Unit =
   {
     val table =
-      (Multi_Map.empty[String, String] /: paths)({ case (tab, path) =>
+      paths.foldLeft(Multi_Map.empty[String, String]) { case (tab, path) =>
         val name = path.expand.implode
         tab.insert(Word.lowercase(name), name)
-      })
+      }
     val collisions =
       (for { (_, coll) <- table.iterator_list if coll.length > 1 } yield coll).toList.flatten
     if (collisions.nonEmpty) {
--- a/src/Pure/General/pretty.scala	Wed Mar 03 22:48:46 2021 +0100
+++ b/src/Pure/General/pretty.scala	Thu Mar 04 15:41:46 2021 +0100
@@ -75,7 +75,7 @@
     {
       val (line, rest) =
         Library.take_prefix[Tree]({ case Break(true, _, _) => false case _ => true }, prts)
-      val len1 = ((0.0 /: line) { case (l, t) => l + t.length }) max len
+      val len1 = (line.foldLeft(0.0) { case (l, t) => l + t.length }) max len
       (rest: @unchecked) match {
         case Break(true, _, ind) :: rest1 =>
           body_length(Break(false, indent1 + ind, 0) :: rest1, len1)
--- a/src/Pure/General/scan.scala	Wed Mar 03 22:48:46 2021 +0100
+++ b/src/Pure/General/scan.scala	Thu Mar 04 15:41:46 2021 +0100
@@ -323,9 +323,9 @@
     /* auxiliary operations */
 
     private def dest(tree: Lexicon.Tree, result: List[String]): List[String] =
-      (result /: tree.branches.toList) ((res, entry) =>
-        entry match { case (_, (s, tr)) =>
-          if (s.isEmpty) dest(tr, res) else dest(tr, s :: res) })
+      tree.branches.toList.foldLeft(result) {
+        case (res, (_, (s, tr))) => if (s.isEmpty) dest(tr, res) else dest(tr, s :: res)
+      }
 
     private def lookup(str: CharSequence): Option[(Boolean, Lexicon.Tree)] =
     {
@@ -390,7 +390,7 @@
         new Lexicon(extend(rep, 0))
       }
 
-    def ++ (elems: IterableOnce[String]): Lexicon = (this /: elems)(_ + _)
+    def ++ (elems: IterableOnce[String]): Lexicon = elems.foldLeft(this)(_ + _)
 
     def ++ (other: Lexicon): Lexicon =
       if (this eq other) this
--- a/src/Pure/General/symbol.scala	Wed Mar 03 22:48:46 2021 +0100
+++ b/src/Pure/General/symbol.scala	Thu Mar 04 15:41:46 2021 +0100
@@ -336,14 +336,14 @@
     }
 
     private val symbols: List[(Symbol, Properties.T)] =
-      (((List.empty[(Symbol, Properties.T)], Set.empty[Symbol]) /:
-          split_lines(symbols_spec).reverse)
-        { case (res, No_Decl()) => res
+      split_lines(symbols_spec).reverse.
+        foldLeft((List.empty[(Symbol, Properties.T)], Set.empty[Symbol])) {
+          case (res, No_Decl()) => res
           case ((list, known), decl) =>
             val (sym, props) = read_decl(decl)
             if (known(sym)) (list, known)
             else ((sym, props) :: list, known + sym)
-        })._1
+        }._1
 
 
     /* basic properties */
--- a/src/Pure/Isar/document_structure.scala	Wed Mar 03 22:48:46 2021 +0100
+++ b/src/Pure/Isar/document_structure.scala	Thu Mar 04 15:41:46 2021 +0100
@@ -17,7 +17,7 @@
 
   sealed abstract class Document { def length: Int }
   case class Block(name: String, text: String, body: List[Document]) extends Document
-  { val length: Int = (0 /: body)(_ + _.length) }
+  { val length: Int = body.foldLeft(0)(_ + _.length) }
   case class Atom(length: Int) extends Document
 
   def is_theory_command(keywords: Keyword.Keywords, command: Command): Boolean =
--- a/src/Pure/Isar/keyword.scala	Wed Mar 03 22:48:46 2021 +0100
+++ b/src/Pure/Isar/keyword.scala	Thu Mar 04 15:41:46 2021 +0100
@@ -160,13 +160,15 @@
         val kinds1 =
           if (kinds eq other.kinds) kinds
           else if (kinds.isEmpty) other.kinds
-          else (kinds /: other.kinds) { case (m, e) => if (m.isDefinedAt(e._1)) m else m + e }
+          else other.kinds.foldLeft(kinds) { case (m, e) => if (m.isDefinedAt(e._1)) m else m + e }
         val load_commands1 =
           if (load_commands eq other.load_commands) load_commands
           else if (load_commands.isEmpty) other.load_commands
-          else
-            (load_commands /: other.load_commands) {
-              case (m, e) => if (m.isDefinedAt(e._1)) m else m + e }
+          else {
+            other.load_commands.foldLeft(load_commands) {
+              case (m, e) => if (m.isDefinedAt(e._1)) m else m + e
+            }
+          }
         new Keywords(kinds1, load_commands1)
       }
 
@@ -187,7 +189,7 @@
     }
 
     def add_keywords(header: Thy_Header.Keywords): Keywords =
-      (this /: header) {
+      header.foldLeft(this) {
         case (keywords, (name, spec)) =>
           if (spec.kind.isEmpty)
             keywords + Symbol.decode(name) + Symbol.encode(name)
@@ -217,13 +219,12 @@
     /* lexicons */
 
     private def make_lexicon(is_minor: Boolean): Scan.Lexicon =
-      (Scan.Lexicon.empty /: kinds)(
-        {
-          case (lex, (name, kind)) =>
-            if ((kind == "" || kind == BEFORE_COMMAND || kind == QUASI_COMMAND) == is_minor)
-              lex + name
-            else lex
-        })
+      kinds.foldLeft(Scan.Lexicon.empty) {
+        case (lex, (name, kind)) =>
+          if ((kind == "" || kind == BEFORE_COMMAND || kind == QUASI_COMMAND) == is_minor)
+            lex + name
+          else lex
+      }
 
     lazy val minor: Scan.Lexicon = make_lexicon(true)
     lazy val major: Scan.Lexicon = make_lexicon(false)
--- a/src/Pure/Isar/line_structure.scala	Wed Mar 03 22:48:46 2021 +0100
+++ b/src/Pure/Isar/line_structure.scala	Thu Mar 04 15:41:46 2021 +0100
@@ -45,7 +45,7 @@
       else span_depth
 
     val (span_depth1, after_span_depth1, element_depth1) =
-      ((span_depth, after_span_depth, element_depth) /: tokens) {
+      tokens.foldLeft((span_depth, after_span_depth, element_depth)) {
         case (depths @ (x, y, z), tok) =>
           if (tok.is_begin) (z + 2, z + 1, z + 1)
           else if (tok.is_end) (z + 1, z - 1, z - 1)
--- a/src/Pure/Isar/outer_syntax.scala	Wed Mar 03 22:48:46 2021 +0100
+++ b/src/Pure/Isar/outer_syntax.scala	Thu Mar 04 15:41:46 2021 +0100
@@ -16,7 +16,7 @@
 
   val empty: Outer_Syntax = new Outer_Syntax()
 
-  def merge(syns: List[Outer_Syntax]): Outer_Syntax = (empty /: syns)(_ ++ _)
+  def merge(syns: List[Outer_Syntax]): Outer_Syntax = syns.foldLeft(empty)(_ ++ _)
 
 
   /* string literals */
@@ -61,7 +61,7 @@
       keywords + (name, kind, load_command), rev_abbrevs, language_context, has_tokens = true)
 
   def add_keywords(keywords: Thy_Header.Keywords): Outer_Syntax =
-    (this /: keywords) {
+    keywords.foldLeft(this) {
       case (syntax, (name, spec)) =>
         syntax +
           (Symbol.decode(name), spec.kind, spec.load_command) +
@@ -177,8 +177,9 @@
             case Some(cmd) =>
               val name = cmd.source
               val offset =
-                (0 /: content.takeWhile(_ != cmd)) {
-                  case (i, tok) => i + Symbol.length(tok.source) }
+                content.takeWhile(_ != cmd).foldLeft(0) {
+                  case (i, tok) => i + Symbol.length(tok.source)
+                }
               val end_offset = offset + Symbol.length(name)
               val range = Text.Range(offset, end_offset) + 1
               Command_Span.Command_Span(name, Position.Range(range))
--- a/src/Pure/ML/ml_statistics.scala	Wed Mar 03 22:48:46 2021 +0100
+++ b/src/Pure/ML/ml_statistics.scala	Thu Mar 04 15:41:46 2021 +0100
@@ -268,7 +268,7 @@
   /* content */
 
   def maximum(field: String): Double =
-    (0.0 /: content)({ case (m, e) => m max e.get(field) })
+    content.foldLeft(0.0) { case (m, e) => m max e.get(field) }
 
   def average(field: String): Double =
   {
--- a/src/Pure/PIDE/command.scala	Wed Mar 03 22:48:46 2021 +0100
+++ b/src/Pure/PIDE/command.scala	Thu Mar 04 15:41:46 2021 +0100
@@ -56,8 +56,8 @@
   {
     type Entry = (Long, XML.Elem)
     val empty: Results = new Results(SortedMap.empty)
-    def make(args: IterableOnce[Results.Entry]): Results = (empty /: args)(_ + _)
-    def merge(args: IterableOnce[Results]): Results = (empty /: args)(_ ++ _)
+    def make(args: IterableOnce[Results.Entry]): Results = args.foldLeft(empty)(_ + _)
+    def merge(args: IterableOnce[Results]): Results = args.foldLeft(empty)(_ ++ _)
   }
 
   final class Results private(private val rep: SortedMap[Long, XML.Elem])
@@ -74,7 +74,7 @@
     def ++ (other: Results): Results =
       if (this eq other) this
       else if (rep.isEmpty) other
-      else (this /: other.iterator)(_ + _)
+      else other.iterator.foldLeft(this)(_ + _)
 
     override def hashCode: Int = rep.hashCode
     override def equals(that: Any): Boolean =
@@ -92,7 +92,7 @@
   {
     type Entry = (Long, Export.Entry)
     val empty: Exports = new Exports(SortedMap.empty)
-    def merge(args: IterableOnce[Exports]): Exports = (empty /: args)(_ ++ _)
+    def merge(args: IterableOnce[Exports]): Exports = args.foldLeft(empty)(_ ++ _)
   }
 
   final class Exports private(private val rep: SortedMap[Long, Export.Entry])
@@ -107,7 +107,7 @@
     def ++ (other: Exports): Exports =
       if (this eq other) this
       else if (rep.isEmpty) other
-      else (this /: other.iterator)(_ + _)
+      else other.iterator.foldLeft(this)(_ + _)
 
     override def hashCode: Int = rep.hashCode
     override def equals(that: Any): Boolean =
@@ -134,8 +134,8 @@
     type Entry = (Markup_Index, Markup_Tree)
     val empty: Markups = new Markups(Map.empty)
     def init(markup: Markup_Tree): Markups = new Markups(Map(Markup_Index.markup -> markup))
-    def make(args: IterableOnce[Entry]): Markups = (empty /: args)(_ + _)
-    def merge(args: IterableOnce[Markups]): Markups = (empty /: args)(_ ++ _)
+    def make(args: IterableOnce[Entry]): Markups = args.foldLeft(empty)(_ + _)
+    def merge(args: IterableOnce[Markups]): Markups = args.foldLeft(empty)(_ ++ _)
   }
 
   final class Markups private(private val rep: Map[Markup_Index, Markup_Tree])
@@ -157,7 +157,7 @@
     def ++ (other: Markups): Markups =
       if (this eq other) this
       else if (rep.isEmpty) other
-      else (this /: other.rep.iterator)(_ + _)
+      else other.rep.iterator.foldLeft(this)(_ + _)
 
     def redirection_iterator: Iterator[Document_ID.Generic] =
       for (Markup_Index(_, Symbol.Text_Chunk.Id(id)) <- rep.keysIterator)
@@ -295,21 +295,23 @@
         case XML.Elem(Markup(Markup.STATUS, _), msgs) =>
           if (command.span.is_theory) this
           else {
-            (this /: msgs)((state, msg) =>
-              msg match {
-                case elem @ XML.Elem(markup, Nil) =>
-                  state.
-                    add_status(markup).
-                    add_markup(true, Symbol.Text_Chunk.Default, Text.Info(command.core_range, elem))
-                case _ =>
-                  Output.warning("Ignored status message: " + msg)
-                  state
-              })
+            msgs.foldLeft(this) {
+              case (state, msg) =>
+                msg match {
+                  case elem @ XML.Elem(markup, Nil) =>
+                    state.
+                      add_status(markup).
+                      add_markup(true, Symbol.Text_Chunk.Default, Text.Info(command.core_range, elem))
+                  case _ =>
+                    Output.warning("Ignored status message: " + msg)
+                    state
+                }
+            }
           }
 
         case XML.Elem(Markup(Markup.REPORT, atts0), msgs) =>
-          (this /: msgs)((state, msg) =>
-            {
+          msgs.foldLeft(this) {
+            case (state, msg) =>
               def bad(): Unit = Output.warning("Ignored report message: " + msg)
 
               msg match {
@@ -342,7 +344,7 @@
                   }
                 case _ => bad(); state
               }
-            })
+          }
 
         case XML.Elem(Markup(name, props), body) =>
           props match {
@@ -562,7 +564,7 @@
 
   val core_range: Text.Range =
     Text.Range(0,
-      (length /: span.content.reverse.iterator.takeWhile(_.is_ignored))(_ - _.source.length))
+      span.content.reverse.iterator.takeWhile(_.is_ignored).foldLeft(length)(_ - _.source.length))
 
   def source(range: Text.Range): String = range.substring(source)
 
--- a/src/Pure/PIDE/command_span.scala	Wed Mar 03 22:48:46 2021 +0100
+++ b/src/Pure/PIDE/command_span.scala	Thu Mar 04 15:41:46 2021 +0100
@@ -74,7 +74,7 @@
     def keyword_pos(start: Token.Pos): Token.Pos =
       kind match {
         case _: Command_Span =>
-          (start /: content.iterator.takeWhile(tok => !tok.is_command))(_.advance(_))
+          content.iterator.takeWhile(tok => !tok.is_command).foldLeft(start)(_.advance(_))
         case _ => start
       }
 
@@ -89,7 +89,7 @@
 
     def content_reader: CharSequenceReader = Scan.char_reader(Token.implode(content))
 
-    def length: Int = (0 /: content)(_ + _.source.length)
+    def length: Int = content.foldLeft(0)(_ + _.source.length)
 
     def compact_source: (String, Span) =
     {
--- a/src/Pure/PIDE/document.scala	Wed Mar 03 22:48:46 2021 +0100
+++ b/src/Pure/PIDE/document.scala	Thu Mar 04 15:41:46 2021 +0100
@@ -246,7 +246,7 @@
         var p = pos
         for (command <- commands) yield {
           val start = p
-          p = (p /: command.span.content)(_.advance(_))
+          p = command.span.content.foldLeft(p)(_.advance(_))
           (command, start)
         }
       }
@@ -385,7 +385,7 @@
     def purge_suppressed: Option[Nodes] =
       graph.keys_iterator.filter(is_suppressed).toList match {
         case Nil => None
-        case del => Some(new Nodes((graph /: del)(_.del_node(_))))
+        case del => Some(new Nodes(del.foldLeft(graph)(_.del_node(_))))
       }
 
     def + (entry: (Node.Name, Node)): Nodes =
@@ -393,9 +393,12 @@
       val (name, node) = entry
       val imports = node.header.imports
       val graph1 =
-        (graph.default_node(name, Node.empty) /: imports)((g, p) => g.default_node(p, Node.empty))
-      val graph2 = (graph1 /: graph1.imm_preds(name))((g, dep) => g.del_edge(dep, name))
-      val graph3 = (graph2 /: imports)((g, dep) => g.add_edge(dep, name))
+        imports.foldLeft(graph.default_node(name, Node.empty)) {
+          case (g, p) => g.default_node(p, Node.empty)
+        }
+      val graph2 =
+        graph1.imm_preds(name).foldLeft(graph1) { case (g, dep) => g.del_edge(dep, name) }
+      val graph3 = imports.foldLeft(graph2) { case (g, dep) => g.add_edge(dep, name) }
       new Nodes(graph3.map_node(name, _ => node))
     }
 
@@ -449,8 +452,8 @@
     def purge_suppressed(
       versions: Map[Document_ID.Version, Version]): Map[Document_ID.Version, Version] =
     {
-      (versions /:
-        (for ((id, v) <- versions.iterator; v1 <- v.purge_suppressed) yield (id, v1)))(_ + _)
+      (for ((id, v) <- versions.iterator; v1 <- v.purge_suppressed) yield (id, v1)).
+        foldLeft(versions)(_ + _)
     }
   }
 
@@ -567,9 +570,9 @@
     private lazy val reverse_edits = edits.reverse
 
     def convert(offset: Text.Offset): Text.Offset =
-      (offset /: edits)((i, edit) => edit.convert(i))
+      edits.foldLeft(offset) { case (i, edit) => edit.convert(i) }
     def revert(offset: Text.Offset): Text.Offset =
-      (offset /: reverse_edits)((i, edit) => edit.revert(i))
+      reverse_edits.foldLeft(offset) { case (i, edit) => edit.revert(i) }
 
     def convert(range: Text.Range): Text.Range = range.map(convert)
     def revert(range: Text.Range): Text.Range = range.map(revert)
@@ -683,7 +686,7 @@
           node.commands.iterator.takeWhile(_ != command).map(_.source) ++
             (if (offset == 0) Iterator.empty
              else Iterator.single(command.source(Text.Range(0, command.chunk.decode(offset)))))
-        val pos = (Line.Position.zero /: sources_iterator)(_.advance(_))
+        val pos = sources_iterator.foldLeft(Line.Position.zero)(_.advance(_))
         Line.Node_Position(name, pos)
       }
 
@@ -842,7 +845,7 @@
       {
         require(!is_finished, "assignment already finished")
         val command_execs1 =
-          (command_execs /: update) {
+          update.foldLeft(command_execs) {
             case (res, (command_id, exec_ids)) =>
               if (exec_ids.isEmpty) res - command_id
               else res + (command_id -> exec_ids)
@@ -928,8 +931,10 @@
     }
 
     private def redirection(st: Command.State): Graph[Document_ID.Command, Unit] =
-      (commands_redirection /: st.markups.redirection_iterator)({ case (graph, id) =>
-        graph.default_node(id, ()).default_node(st.command.id, ()).add_edge(id, st.command.id) })
+      st.markups.redirection_iterator.foldLeft(commands_redirection) {
+        case (graph, id) =>
+          graph.default_node(id, ()).default_node(st.command.id, ()).add_edge(id, st.command.id)
+      }
 
     def accumulate(id: Document_ID.Generic, message: XML.Elem, cache: XML.Cache)
       : (Command.State, State) =
@@ -1022,7 +1027,7 @@
         if (execs.isDefinedAt(exec_id)) None else Some(exec_id -> st)
 
       val (changed_commands, new_execs) =
-        ((Nil: List[Command], execs) /: update) {
+        update.foldLeft((Nil: List[Command], execs)) {
           case ((commands1, execs1), (command_id, exec)) =>
             val st = the_static_state(command_id)
             val command = st.command
@@ -1250,10 +1255,10 @@
         } yield edits
 
       val edits =
-        (pending_edits /: rev_pending_changes)({
+        rev_pending_changes.foldLeft(pending_edits) {
           case (edits, Node.Edits(es)) => es ::: edits
           case (edits, _) => edits
-        })
+        }
 
       new Snapshot(this, version, node_name, edits, snippet_command)
     }
--- a/src/Pure/PIDE/document_status.scala	Wed Mar 03 22:48:46 2021 +0100
+++ b/src/Pure/PIDE/document_status.scala	Thu Mar 04 15:41:46 2021 +0100
@@ -60,7 +60,7 @@
     def merge(status_iterator: Iterator[Command_Status]): Command_Status =
       if (status_iterator.hasNext) {
         val status0 = status_iterator.next()
-        (status0 /: status_iterator)(_ + _)
+        status_iterator.foldLeft(status0)(_ + _)
       }
       else empty
   }
@@ -198,10 +198,10 @@
         st <- state.command_states(version, command)
       } {
         val command_timing =
-          (0.0 /: st.status)({
+          st.status.foldLeft(0.0) {
             case (timing, Markup.Timing(t)) => timing + t.elapsed.seconds
             case (timing, _) => timing
-          })
+          }
         total += command_timing
         if (command_timing > 0.0 && command_timing >= threshold) {
           command_timings += (command -> command_timing)
--- 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 =
       {
--- a/src/Pure/PIDE/line.scala	Wed Mar 03 22:48:46 2021 +0100
+++ b/src/Pure/PIDE/line.scala	Thu Mar 04 15:41:46 2021 +0100
@@ -118,7 +118,7 @@
 
     private def length(lines: List[Line]): Int =
       if (lines.isEmpty) 0
-      else ((0 /: lines) { case (n, line) => n + line.text.length + 1 }) - 1
+      else (lines.foldLeft(0) { case (n, line) => n + line.text.length + 1 }) - 1
 
     def text(lines: List[Line]): String = lines.mkString("", "\n", "")
   }
@@ -169,7 +169,7 @@
       if (0 <= l && l < n) {
         if (0 <= c && c <= lines(l).text.length) {
           val line_offset =
-            (0 /: lines.iterator.take(l)) { case (n, line) => n + line.text.length + 1 }
+            lines.iterator.take(l).foldLeft(0) { case (n, line) => n + line.text.length + 1 }
           Some(line_offset + c)
         }
         else None
--- a/src/Pure/PIDE/markup_tree.scala	Wed Mar 03 22:48:46 2021 +0100
+++ b/src/Pure/PIDE/markup_tree.scala	Thu Mar 04 15:41:46 2021 +0100
@@ -20,16 +20,16 @@
   val empty: Markup_Tree = new Markup_Tree(Branches.empty)
 
   def merge(trees: List[Markup_Tree], range: Text.Range, elements: Markup.Elements): Markup_Tree =
-    (empty /: trees)(_.merge(_, range, elements))
+    trees.foldLeft(empty)(_.merge(_, range, elements))
 
   def merge_disjoint(trees: List[Markup_Tree]): Markup_Tree =
     trees match {
       case Nil => empty
       case head :: tail =>
         new Markup_Tree(
-          (head.branches /: tail) {
+          tail.foldLeft(head.branches) {
             case (branches, tree) =>
-              (branches /: tree.branches) {
+              tree.branches.foldLeft(branches) {
                 case (bs, (r, entry)) =>
                   require(!bs.isDefinedAt(r), "cannot merge markup trees")
                   bs + (r -> entry)
@@ -93,7 +93,8 @@
           (offset + XML.text_length(body), markup_trees)
 
         case (elems, body) =>
-          val (end_offset, subtrees) = ((offset, Nil: List[Markup_Tree]) /: body)(make_trees)
+          val (end_offset, subtrees) =
+             body.foldLeft((offset, Nil: List[Markup_Tree]))(make_trees)
           if (offset == end_offset) acc
           else {
             val range = Text.Range(offset, end_offset)
@@ -104,7 +105,7 @@
     }
 
   def from_XML(body: XML.Body): Markup_Tree =
-    merge_disjoint(((0, Nil: List[Markup_Tree]) /: body)(make_trees)._2)
+    merge_disjoint(body.foldLeft((0, Nil: List[Markup_Tree]))(make_trees)._2)
 }
 
 
@@ -163,13 +164,15 @@
   def merge(other: Markup_Tree, root_range: Text.Range, elements: Markup.Elements): Markup_Tree =
   {
     def merge_trees(tree1: Markup_Tree, tree2: Markup_Tree): Markup_Tree =
-      (tree1 /: tree2.branches)(
-        { case (tree, (range, entry)) =>
-            if (!range.overlaps(root_range)) tree
-            else
-              (merge_trees(tree, entry.subtree) /: entry.filter_markup(elements))(
-                { case (t, elem) => t + Text.Info(range, elem) })
-        })
+      tree2.branches.foldLeft(tree1) {
+        case (tree, (range, entry)) =>
+          if (!range.overlaps(root_range)) tree
+          else {
+            entry.filter_markup(elements).foldLeft(merge_trees(tree, entry.subtree)) {
+              case (t, elem) => t + Text.Info(range, elem)
+            }
+          }
+      }
 
     if (this eq other) this
     else {
@@ -236,7 +239,7 @@
       else List(XML.Text(text.subSequence(start, stop).toString))
 
     def make_elems(rev_markups: List[XML.Elem], body: XML.Body): XML.Body =
-      (body /: rev_markups) {
+      rev_markups.foldLeft(body) {
         case (b, elem) =>
           if (!elements(elem.name)) b
           else if (elem.body.isEmpty) List(XML.Elem(elem.markup, b))
--- a/src/Pure/PIDE/protocol_handlers.scala	Wed Mar 03 22:48:46 2021 +0100
+++ b/src/Pure/PIDE/protocol_handlers.scala	Thu Mar 04 15:41:46 2021 +0100
@@ -74,8 +74,9 @@
   private val state = Synchronized(Protocol_Handlers.State(session))
 
   def prover_options(options: Options): Options =
-    (options /: state.value.handlers)(
-      { case (opts, (_, handler)) => handler.prover_options(opts) })
+    state.value.handlers.foldLeft(options) {
+      case (opts, (_, handler)) => handler.prover_options(opts)
+    }
 
   def get(name: String): Option[Session.Protocol_Handler] = state.value.get(name)
   def init(handler: Session.Protocol_Handler): Unit = state.change(_.init(handler))
--- a/src/Pure/PIDE/prover.scala	Wed Mar 03 22:48:46 2021 +0100
+++ b/src/Pure/PIDE/prover.scala	Thu Mar 04 15:41:46 2021 +0100
@@ -349,7 +349,7 @@
     command_input match {
       case Some(thread) if thread.is_active =>
         if (trace) {
-          val payload = (0 /: args)({ case (n, b) => n + b.length })
+          val payload = args.foldLeft(0) { case (n, b) => n + b.length }
           Output.writeln(
             "protocol_command " + name + ", args = " + args.length + ", payload = " + payload)
         }
--- a/src/Pure/PIDE/rendering.scala	Wed Mar 03 22:48:46 2021 +0100
+++ b/src/Pure/PIDE/rendering.scala	Thu Mar 04 15:41:46 2021 +0100
@@ -177,7 +177,7 @@
     def apply(ids: Set[Long]): Focus = new Focus(ids)
     val empty: Focus = apply(Set.empty)
     def make(args: List[Text.Info[Focus]]): Focus =
-      (empty /: args)({ case (focus1, Text.Info(_, focus2)) => focus1 ++ focus2 })
+      args.foldLeft(empty) { case (focus1, Text.Info(_, focus2)) => focus1 ++ focus2 }
 
     val full: Focus =
       new Focus(Set.empty)
@@ -195,7 +195,7 @@
     def ++ (other: Focus): Focus =
       if (this eq other) this
       else if (rep.isEmpty) other
-      else (this /: other.rep.iterator)(_ + _)
+      else other.rep.iterator.foldLeft(this)(_ + _)
     override def toString: String = rep.mkString("Focus(", ",", ")")
   }
 
@@ -709,7 +709,7 @@
     else {
       val r = Text.Range(results.head.range.start, results.last.range.stop)
       val all_tips =
-        (SortedMap.empty[Long, XML.Tree] /: results.flatMap(_.messages))(_ + _)
+        results.flatMap(_.messages).foldLeft(SortedMap.empty[Long, XML.Tree])(_ + _)
           .iterator.map(_._2).toList :::
         results.flatMap(res => res.infos(true)) :::
         results.flatMap(res => res.infos(false)).lastOption.toList
--- a/src/Pure/PIDE/resources.scala	Wed Mar 03 22:48:46 2021 +0100
+++ b/src/Pure/PIDE/resources.scala	Thu Mar 04 15:41:46 2021 +0100
@@ -291,11 +291,12 @@
   def session_dependencies(info: Sessions.Info, progress: Progress = new Progress)
     : Dependencies[Options] =
   {
-    (Dependencies.empty[Options] /: info.theories)({ case (dependencies, (options, thys)) =>
-      dependencies.require_thys(options,
-        for { (thy, pos) <- thys } yield (import_name(info, thy), pos),
-        progress = progress)
-    })
+    info.theories.foldLeft(Dependencies.empty[Options]) {
+      case (dependencies, (options, thys)) =>
+        dependencies.require_thys(options,
+          for { (thy, pos) <- thys } yield (import_name(info, thy), pos),
+          progress = progress)
+    }
   }
 
   object Dependencies
@@ -361,7 +362,7 @@
         thys: List[(Document.Node.Name, Position.T)],
         progress: Progress = new Progress,
         initiators: List[Document.Node.Name] = Nil): Dependencies[A] =
-      (this /: thys)(_.require_thy(adjunct, _, progress = progress, initiators = initiators))
+      thys.foldLeft(this)(_.require_thy(adjunct, _, progress = progress, initiators = initiators))
 
     def entries: List[Document.Node.Entry] = rev_entries.reverse
 
@@ -392,19 +393,20 @@
     }
 
     lazy val loaded_theories: Graph[String, Outer_Syntax] =
-      (session_base.loaded_theories /: entries)({ case (graph, entry) =>
-        val name = entry.name.theory
-        val imports = entry.header.imports.map(_.theory)
-
-        val graph1 = (graph /: (name :: imports))(_.default_node(_, Outer_Syntax.empty))
-        val graph2 = (graph1 /: imports)(_.add_edge(_, name))
+      entries.foldLeft(session_base.loaded_theories) {
+        case (graph, entry) =>
+          val name = entry.name.theory
+          val imports = entry.header.imports.map(_.theory)
 
-        val syntax0 = if (name == Thy_Header.PURE) List(Thy_Header.bootstrap_syntax) else Nil
-        val syntax1 = (name :: graph2.imm_preds(name).toList).map(graph2.get_node)
-        val syntax = Outer_Syntax.merge(syntax0 ::: syntax1) + entry.header
+          val graph1 = (name :: imports).foldLeft(graph)(_.default_node(_, Outer_Syntax.empty))
+          val graph2 = imports.foldLeft(graph1)(_.add_edge(_, name))
 
-        graph2.map_node(name, _ => syntax)
-      })
+          val syntax0 = if (name == Thy_Header.PURE) List(Thy_Header.bootstrap_syntax) else Nil
+          val syntax1 = (name :: graph2.imm_preds(name).toList).map(graph2.get_node)
+          val syntax = Outer_Syntax.merge(syntax0 ::: syntax1) + entry.header
+
+          graph2.map_node(name, _ => syntax)
+      }
 
     def get_syntax(name: Document.Node.Name): Outer_Syntax =
       loaded_theories.get_node(name.theory)
--- a/src/Pure/PIDE/xml.scala	Wed Mar 03 22:48:46 2021 +0100
+++ b/src/Pure/PIDE/xml.scala	Thu Mar 04 15:41:46 2021 +0100
@@ -101,11 +101,11 @@
   {
     def traverse(x: A, t: Tree): A =
       t match {
-        case XML.Wrapped_Elem(_, _, ts) => (x /: ts)(traverse)
-        case XML.Elem(_, ts) => (x /: ts)(traverse)
+        case XML.Wrapped_Elem(_, _, ts) => ts.foldLeft(x)(traverse)
+        case XML.Elem(_, ts) => ts.foldLeft(x)(traverse)
         case XML.Text(s) => op(x, s)
       }
-    (a /: body)(traverse)
+    body.foldLeft(a)(traverse)
   }
 
   def text_length(body: Body): Int = traverse_text(body)(0) { case (n, s) => n + s.length }
--- a/src/Pure/System/getopts.scala	Wed Mar 03 22:48:46 2021 +0100
+++ b/src/Pure/System/getopts.scala	Thu Mar 04 15:41:46 2021 +0100
@@ -15,7 +15,7 @@
   def apply(usage_text: String, option_specs: (String, String => Unit)*): Getopts =
   {
     val options =
-      (Map.empty[Char, (Boolean, String => Unit)] /: option_specs) {
+      option_specs.foldLeft(Map.empty[Char, (Boolean, String => Unit)]) {
         case (m, (s, f)) =>
           val (a, entry) =
             if (s.size == 1) (s(0), (false, f))
--- a/src/Pure/System/options.scala	Wed Mar 03 22:48:46 2021 +0100
+++ b/src/Pure/System/options.scala	Thu Mar 04 15:41:46 2021 +0100
@@ -119,7 +119,7 @@
           case Success(result, _) => result
           case bad => error(bad.toString)
         }
-      try { (options.set_section("") /: ops) { case (opts, op) => op(opts) } }
+      try { ops.foldLeft(options.set_section("")) { case (opts, op) => op(opts) } }
       catch { case ERROR(msg) => error(msg + Position.here(Position.File(file_name))) }
     }
 
@@ -137,7 +137,7 @@
       dir <- Isabelle_System.components()
       file = dir + OPTIONS if file.is_file
     } { options = Parser.parse_file(options, file.implode, File.read(file)) }
-    (Options.Parser.parse_prefs(options, prefs) /: opts)(_ + _)
+    opts.foldLeft(Options.Parser.parse_prefs(options, prefs))(_ + _)
   }
 
 
@@ -181,9 +181,9 @@
       val options0 = Options.init()
       val options1 =
         if (build_options)
-          (options0 /: Word.explode(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS")))(_ + _)
+          Word.explode(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS")).foldLeft(options0)(_ + _)
         else options0
-      (options1 /: more_options)(_ + _)
+      more_options.foldLeft(options1)(_ + _)
     }
 
     if (get_option != "")
@@ -363,7 +363,7 @@
   }
 
   def ++ (specs: List[Options.Spec]): Options =
-    (this /: specs)({ case (x, (y, z)) => x + (y, z) })
+    specs.foldLeft(this) { case (x, (y, z)) => x + (y, z) }
 
 
   /* sections */
--- a/src/Pure/Thy/bibtex.scala	Wed Mar 03 22:48:46 2021 +0100
+++ b/src/Pure/Thy/bibtex.scala	Thu Mar 04 15:41:46 2021 +0100
@@ -389,7 +389,9 @@
 
     def heading_length: Int =
       if (name == "") 1
-      else (0 /: tokens.takeWhile(tok => !tok.is_open)){ case (n, tok) => n + tok.source.length }
+      else {
+        tokens.takeWhile(tok => !tok.is_open).foldLeft(0) { case (n, tok) => n + tok.source.length }
+      }
 
     def is_ignored: Boolean = kind == "" && tokens.forall(_.is_ignored)
     def is_malformed: Boolean = kind == "" || tokens.exists(_.is_malformed)
--- a/src/Pure/Thy/export_theory.scala	Wed Mar 03 22:48:46 2021 +0100
+++ b/src/Pure/Thy/export_theory.scala	Thu Mar 04 15:41:46 2021 +0100
@@ -48,12 +48,16 @@
         }))
 
     val graph0 =
-      (Graph.string[Option[Theory]] /: thys) {
-        case (g, thy) => g.default_node(thy.name, Some(thy)) }
+      thys.foldLeft(Graph.string[Option[Theory]]) {
+        case (g, thy) => g.default_node(thy.name, Some(thy))
+      }
     val graph1 =
-      (graph0 /: thys) { case (g0, thy) =>
-        (g0 /: thy.parents) { case (g1, parent) =>
-          g1.default_node(parent, None).add_edge_acyclic(parent, thy.name) } }
+      thys.foldLeft(graph0) {
+        case (g0, thy) =>
+          thy.parents.foldLeft(g0) {
+            case (g1, parent) => g1.default_node(parent, None).add_edge_acyclic(parent, thy.name)
+          }
+      }
 
     Session(session_name, graph1)
   }
--- a/src/Pure/Thy/file_format.scala	Wed Mar 03 22:48:46 2021 +0100
+++ b/src/Pure/Thy/file_format.scala	Thu Mar 04 15:41:46 2021 +0100
@@ -39,7 +39,7 @@
       agents.mkString("File_Format.Session(", ", ", ")")
 
     def prover_options(options: Options): Options =
-      (options /: agents)({ case (opts, agent) => agent.prover_options(opts) })
+      agents.foldLeft(options) { case (opts, agent) => agent.prover_options(opts) }
 
     def stop_session: Unit = agents.foreach(_.stop)
   }
--- a/src/Pure/Thy/latex.scala	Wed Mar 03 22:48:46 2021 +0100
+++ b/src/Pure/Thy/latex.scala	Thu Mar 04 15:41:46 2021 +0100
@@ -67,8 +67,8 @@
         case None => None
         case Some(file) =>
           val source_line =
-            (0 /: source_lines.iterator.takeWhile({ case (m, _) => m <= l }))(
-              { case (_, (_, n)) => n })
+            source_lines.iterator.takeWhile({ case (m, _) => m <= l }).
+              foldLeft(0) { case (_, (_, n)) => n }
           if (source_line == 0) None else Some(Position.Line_File(source_line, file))
       }
 
--- a/src/Pure/Thy/sessions.scala	Wed Mar 03 22:48:46 2021 +0100
+++ b/src/Pure/Thy/sessions.scala	Thu Mar 04 15:41:46 2021 +0100
@@ -156,7 +156,7 @@
     }
 
     val session_bases =
-      (Map("" -> sessions_structure.bootstrap) /: sessions_structure.imports_topological_order)({
+      sessions_structure.imports_topological_order.foldLeft(Map("" -> sessions_structure.bootstrap)) {
         case (session_bases, session_name) =>
           progress.expose_interrupt()
 
@@ -230,22 +230,24 @@
                   .transitive_reduction_acyclic
 
               val graph0 =
-                (Graph_Display.empty_graph /: required_subgraph.topological_order)(
-                  { case (g, session) =>
-                      val a = session_node(session)
-                      val bs = required_subgraph.imm_preds(session).toList.map(session_node)
-                      ((g /: (a :: bs))(_.default_node(_, Nil)) /: bs)(_.add_edge(_, a)) })
+                required_subgraph.topological_order.foldLeft(Graph_Display.empty_graph) {
+                  case (g, session) =>
+                    val a = session_node(session)
+                    val bs = required_subgraph.imm_preds(session).toList.map(session_node)
+                    bs.foldLeft((a :: bs).foldLeft(g)(_.default_node(_, Nil)))(_.add_edge(_, a))
+                }
 
-              (graph0 /: dependencies.entries)(
-                { case (g, entry) =>
-                    val a = node(entry.name)
-                    val bs = entry.header.imports.map(node).filterNot(_ == a)
-                    ((g /: (a :: bs))(_.default_node(_, Nil)) /: bs)(_.add_edge(_, a)) })
+              dependencies.entries.foldLeft(graph0) {
+                case (g, entry) =>
+                  val a = node(entry.name)
+                  val bs = entry.header.imports.map(node).filterNot(_ == a)
+                  bs.foldLeft((a :: bs).foldLeft(g)(_.default_node(_, Nil)))(_.add_edge(_, a))
+              }
             }
 
             val known_theories =
-              (deps_base.known_theories /:
-                dependencies.entries.iterator.map(entry => entry.name.theory -> entry))(_ + _)
+              dependencies.entries.iterator.map(entry => entry.name.theory -> entry).
+                foldLeft(deps_base.known_theories)(_ + _)
 
             val known_loaded_files = deps_base.known_loaded_files ++ loaded_files
 
@@ -357,7 +359,7 @@
               cat_error(msg, "The error(s) above occurred in session " +
                 quote(info.name) + Position.here(info.pos))
           }
-      })
+      }
 
     Deps(sessions_structure, session_bases)
   }
@@ -489,14 +491,13 @@
       val imports_bases = imports.map(session_bases)
       parent_base.copy(
         known_theories =
-          (parent_base.known_theories /:
-            (for {
-              base <- imports_bases.iterator
-              (_, entry) <- base.known_theories.iterator
-            } yield (entry.name.theory -> entry)))(_ + _),
+          (for {
+            base <- imports_bases.iterator
+            (_, entry) <- base.known_theories.iterator
+          } yield (entry.name.theory -> entry)).foldLeft(parent_base.known_theories)(_ + _),
         known_loaded_files =
-          (parent_base.known_loaded_files /:
-            imports_bases.iterator.map(_.known_loaded_files))(_ ++ _))
+          imports_bases.iterator.map(_.known_loaded_files).
+            foldLeft(parent_base.known_loaded_files)(_ ++ _))
     }
 
     def dirs: List[Path] = dir :: directories
@@ -661,13 +662,14 @@
                   cycle.map(c => quote(c.toString)).mkString(" via "))) + Position.here(pos))
           }
         }
-        (graph /: graph.iterator) {
-          case (g, (name, (info, _))) => (g /: edges(info))(add_edge(info.pos, name, _, _))
+        graph.iterator.foldLeft(graph) {
+          case (g, (name, (info, _))) =>
+            edges(info).foldLeft(g)(add_edge(info.pos, name, _, _))
         }
       }
 
       val info_graph =
-        (Graph.string[Info] /: infos) {
+        infos.foldLeft(Graph.string[Info]) {
           case (graph, info) =>
             if (graph.defined(info.name))
               error("Duplicate session " + quote(info.name) + Position.here(info.pos) +
@@ -681,12 +683,12 @@
         (for ((name, (info, _)) <- info_graph.iterator) yield (name, info.pos)).toList
 
       val session_directories: Map[JFile, String] =
-        (Map.empty[JFile, String] /:
-          (for {
-            session <- imports_graph.topological_order.iterator
-            info = info_graph.get_node(session)
-            dir <- info.dirs.iterator
-          } yield (info, dir)))({ case (dirs, (info, dir)) =>
+        (for {
+          session <- imports_graph.topological_order.iterator
+          info = info_graph.get_node(session)
+          dir <- info.dirs.iterator
+        } yield (info, dir)).foldLeft(Map.empty[JFile, String]) {
+            case (dirs, (info, dir)) =>
               val session = info.name
               val canonical_dir = dir.canonical_file
               dirs.get(canonical_dir) match {
@@ -697,22 +699,22 @@
                     "\n  vs. session " + quote(session) + Position.here(info.pos))
                 case None => dirs + (canonical_dir -> session)
               }
-            })
+          }
 
       val global_theories: Map[String, String] =
-        (Thy_Header.bootstrap_global_theories.toMap /:
-          (for {
-            session <- imports_graph.topological_order.iterator
-            info = info_graph.get_node(session)
-            thy <- info.global_theories.iterator }
-           yield (info, thy)))({ case (global, (info, thy)) =>
+        (for {
+          session <- imports_graph.topological_order.iterator
+          info = info_graph.get_node(session)
+          thy <- info.global_theories.iterator }
+          yield (info, thy)).foldLeft(Thy_Header.bootstrap_global_theories.toMap) {
+            case (global, (info, thy)) =>
               val qualifier = info.name
               global.get(thy) match {
                 case Some(qualifier1) if qualifier != qualifier1 =>
                   error("Duplicate global theory " + quote(thy) + Position.here(info.pos))
                 case _ => global + (thy -> qualifier)
               }
-            })
+          }
 
       new Structure(
         session_positions, session_directories, global_theories, build_graph, imports_graph)
@@ -739,9 +741,10 @@
         yield (File.standard_path(file), session)
 
     lazy val chapters: SortedMap[String, List[Info]] =
-      (SortedMap.empty[String, List[Info]] /: build_graph.iterator)(
-        { case (chs, (_, (info, _))) =>
-            chs + (info.chapter -> (info :: chs.getOrElse(info.chapter, Nil))) })
+      build_graph.iterator.foldLeft(SortedMap.empty[String, List[Info]]) {
+        case (chs, (_, (info, _))) =>
+          chs + (info.chapter -> (info :: chs.getOrElse(info.chapter, Nil)))
+      }
 
     def build_graph_display: Graph_Display.Graph = Graph_Display.make_graph(build_graph)
     def imports_graph_display: Graph_Display.Graph = Graph_Display.make_graph(imports_graph)
@@ -1061,13 +1064,14 @@
       } yield res
 
     val unique_roots =
-      ((Map.empty[JFile, (Boolean, Path)] /: roots) { case (m, (select, path)) =>
-        val file = path.canonical_file
-        m.get(file) match {
-          case None => m + (file -> (select, path))
-          case Some((select1, path1)) => m + (file -> (select1 || select, path1))
-        }
-      }).toList.map(_._2)
+      roots.foldLeft(Map.empty[JFile, (Boolean, Path)]) {
+        case (m, (select, path)) =>
+          val file = path.canonical_file
+          m.get(file) match {
+            case None => m + (file -> (select, path))
+            case Some((select1, path1)) => m + (file -> (select1 || select, path1))
+          }
+      }.toList.map(_._2)
 
     Structure.make(unique_roots.flatMap(p => read_root(options, p._1, p._2)) ::: infos)
   }
--- a/src/Pure/Thy/thy_header.scala	Wed Mar 03 22:48:46 2021 +0100
+++ b/src/Pure/Thy/thy_header.scala	Thu Mar 04 15:41:46 2021 +0100
@@ -223,7 +223,7 @@
     val (skip_tokens, tokens) = read_tokens(Scan.char_reader(text), strict)
     val pos =
       if (command) Token.Pos.command
-      else (Token.Pos.file(node_name.node) /: skip_tokens)(_ advance _)
+      else skip_tokens.foldLeft(Token.Pos.file(node_name.node))(_ advance _)
 
     Parser.parse_header(tokens, pos).map(Symbol.decode).check(node_name)
   }
--- a/src/Pure/Thy/thy_syntax.scala	Wed Mar 03 22:48:46 2021 +0100
+++ b/src/Pure/Thy/thy_syntax.scala	Thu Mar 04 15:41:46 2021 +0100
@@ -191,7 +191,7 @@
         val inserted =
           blobs_spans2.map({ case (blobs, span) =>
             Command(Document_ID.make(), node_name, blobs, span) })
-        (commands /: cmds2)(_ - _).append_after(hook, inserted)
+        cmds2.foldLeft(commands)(_ - _).append_after(hook, inserted)
     }
   }
 
@@ -310,12 +310,12 @@
       if (edits.isEmpty) (Nil, Document.Version.make(previous.nodes))
       else {
         val reparse =
-          (syntax_changed /: nodes0.iterator)({
+          nodes0.iterator.foldLeft(syntax_changed) {
             case (reparse, (name, node)) =>
               if (node.load_commands_changed(doc_blobs) && !reparse.contains(name))
                 name :: reparse
               else reparse
-            })
+          }
         val reparse_set = reparse.toSet
 
         var nodes = nodes0
@@ -338,7 +338,7 @@
                     commands, commands.head, commands.last))
               else node
             val node2 =
-              (node1 /: edits)(
+              edits.foldLeft(node1)(
                 text_edit(resources, syntax, get_blob, can_import, reparse_limit, _, _))
             val node3 =
               if (reparse_set.contains(name))
--- a/src/Pure/Tools/build.scala	Wed Mar 03 22:48:46 2021 +0100
+++ b/src/Pure/Tools/build.scala	Thu Mar 04 15:41:46 2021 +0100
@@ -159,8 +159,8 @@
     def apply(name: String): Process_Result = results(name)._1.getOrElse(Process_Result(1))
     def info(name: String): Sessions.Info = results(name)._2
     val rc: Int =
-      (0 /: results.iterator.map(
-        { case (_, (Some(r), _)) => r.rc case (_, (None, _)) => 1 }))(_ max _)
+      results.iterator.map({ case (_, (Some(r), _)) => r.rc case (_, (None, _)) => 1 }).
+        foldLeft(0)(_ max _)
     def ok: Boolean = rc == 0
 
     override def toString: String = rc.toString
@@ -661,7 +661,7 @@
     }
 
     val total_timing =
-      (Timing.zero /: results.sessions.iterator.map(a => results(a).timing))(_ + _).
+      results.sessions.iterator.map(a => results(a).timing).foldLeft(Timing.zero)(_ + _).
         copy(elapsed = elapsed_time)
     progress.echo(total_timing.message_resources)
 
--- a/src/Pure/Tools/dump.scala	Wed Mar 03 22:48:46 2021 +0100
+++ b/src/Pure/Tools/dump.scala	Thu Mar 04 15:41:46 2021 +0100
@@ -105,7 +105,7 @@
             "completion_limit=0" +
             "editor_tracing_messages=0" +
             "editor_presentation"
-        (options1 /: aspects)({ case (opts, aspect) => (opts /: aspect.options)(_ + _) })
+        aspects.foldLeft(options1) { case (opts, aspect) => aspect.options.foldLeft(opts)(_ + _) }
       }
 
       val sessions_structure: Sessions.Structure =
--- a/src/Pure/Tools/scala_project.scala	Wed Mar 03 22:48:46 2021 +0100
+++ b/src/Pure/Tools/scala_project.scala	Thu Mar 04 15:41:46 2021 +0100
@@ -53,7 +53,7 @@
   }
 
   lazy val isabelle_scala_files: Map[String, Path] =
-    (Map.empty[String, Path] /: isabelle_files)({
+    isabelle_files.foldLeft(Map.empty[String, Path]) {
       case (map, name) =>
         if (!name.startsWith("src/Tools/jEdit/") && name.endsWith(".scala")) {
           val path = Path.explode("~~/" + name)
@@ -64,7 +64,7 @@
           }
         }
         else map
-    })
+    }
 
   val isabelle_dirs: List[(String, Path)] =
     List(
--- a/src/Pure/Tools/server.scala	Wed Mar 03 22:48:46 2021 +0100
+++ b/src/Pure/Tools/server.scala	Thu Mar 04 15:41:46 2021 +0100
@@ -74,12 +74,13 @@
   }
 
   private lazy val command_table: Map[String, Command] =
-    (Map.empty[String, Command] /: Isabelle_System.make_services(classOf[Commands]).flatMap(_.entries))(
-      { case (cmds, cmd) =>
+    Isabelle_System.make_services(classOf[Commands]).flatMap(_.entries).
+      foldLeft(Map.empty[String, Command]) {
+        case (cmds, cmd) =>
           val name = cmd.command_name
           if (cmds.isDefinedAt(name)) error("Duplicate Isabelle server command: " + quote(name))
           else cmds + (name -> cmd)
-      })
+      }
 
 
   /* output reply */
--- a/src/Tools/Graphview/layout.scala	Wed Mar 03 22:48:46 2021 +0100
+++ b/src/Tools/Graphview/layout.scala	Thu Mar 04 15:41:46 2021 +0100
@@ -108,10 +108,10 @@
             }).toList)
 
       val initial_levels: Levels =
-        (empty_levels /: initial_graph.topological_order) {
+        initial_graph.topological_order.foldLeft(empty_levels) {
           case (levels, vertex) =>
             val level =
-              1 + (-1 /: initial_graph.imm_preds(vertex)) { case (m, v) => m max levels(v) }
+              1 + initial_graph.imm_preds(vertex).foldLeft(-1) { case (m, v) => m max levels(v) }
             levels + (vertex -> level)
         }
 
@@ -121,25 +121,26 @@
       val dummy_info = Info(0.0, 0.0, metrics.dummy_size2, metrics.dummy_size2, Nil)
 
       val (dummy_graph, dummy_levels) =
-        ((initial_graph, initial_levels) /: input_graph.edges_iterator) {
-            case ((graph, levels), (node1, node2)) =>
-              val v1 = Node(node1); val l1 = levels(v1)
-              val v2 = Node(node2); val l2 = levels(v2)
-              if (l2 - l1 <= 1) (graph, levels)
-              else {
-                val dummies_levels =
-                  (for { (l, i) <- ((l1 + 1) until l2).iterator.zipWithIndex }
-                    yield (Dummy(node1, node2, i), l)).toList
-                val dummies = dummies_levels.map(_._1)
+        input_graph.edges_iterator.foldLeft((initial_graph, initial_levels)) {
+          case ((graph, levels), (node1, node2)) =>
+            val v1 = Node(node1); val l1 = levels(v1)
+            val v2 = Node(node2); val l2 = levels(v2)
+            if (l2 - l1 <= 1) (graph, levels)
+            else {
+              val dummies_levels =
+                (for { (l, i) <- ((l1 + 1) until l2).iterator.zipWithIndex }
+                  yield (Dummy(node1, node2, i), l)).toList
+              val dummies = dummies_levels.map(_._1)
 
-                val levels1 = (levels /: dummies_levels)(_ + _)
-                val graph1 =
-                  ((graph /: dummies)(_.new_node(_, dummy_info)).del_edge(v1, v2) /:
-                    (v1 :: dummies ::: List(v2)).sliding(2)) {
-                      case (g, List(a, b)) => g.add_edge(a, b) }
-                (graph1, levels1)
-              }
-          }
+              val levels1 = dummies_levels.foldLeft(levels)(_ + _)
+              val graph1 =
+                (v1 :: dummies ::: List(v2)).sliding(2).
+                  foldLeft(dummies.foldLeft(graph)(_.new_node(_, dummy_info)).del_edge(v1, v2)) {
+                    case (g, List(a, b)) => g.add_edge(a, b)
+                  }
+              (graph1, levels1)
+            }
+        }
 
 
       /* minimize edge crossings and initial coordinates */
@@ -147,25 +148,26 @@
       val levels = minimize_crossings(options, dummy_graph, level_list(dummy_levels))
 
       val levels_graph: Graph =
-        (((dummy_graph, 0.0) /: levels) {
+        levels.foldLeft((dummy_graph, 0.0)) {
           case ((graph, y), level) =>
-            val num_lines = (0 /: level) { case (n, v) => n max graph.get_node(v).lines.length }
-            val num_edges = (0 /: level) { case (n, v) => n + graph.imm_succs(v).size }
+            val num_lines = level.foldLeft(0) { case (n, v) => n max graph.get_node(v).lines.length }
+            val num_edges = level.foldLeft(0) { case (n, v) => n + graph.imm_succs(v).size }
 
             val y1 = y + metrics.node_height2(num_lines)
 
             val graph1 =
-              (((graph, 0.0) /: level) { case ((g, x), v) =>
-                val info = g.get_node(v)
-                val g1 = g.map_node(v, _ => info.copy(x = x + info.width2, y = y1))
-                val x1 = x + info.width + metrics.gap
-                (g1, x1)
-              })._1
+              level.foldLeft((graph, 0.0)) {
+                case ((g, x), v) =>
+                  val info = g.get_node(v)
+                  val g1 = g.map_node(v, _ => info.copy(x = x + info.width2, y = y1))
+                  val x1 = x + info.width + metrics.gap
+                  (g1, x1)
+              }._1
 
             val y2 = y1 + metrics.level_height2(num_lines, num_edges)
 
             (graph1, y2)
-        })._1
+        }._1
 
 
       /* pendulum/rubberband layout */
@@ -188,37 +190,41 @@
     options: Options, graph: Graph, levels: List[Level]): List[Level] =
   {
     def resort(parent: Level, child: Level, top_down: Boolean): Level =
-      child.map(v => {
-          val ps = if (top_down) graph.imm_preds(v) else graph.imm_succs(v)
-          val weight =
-            (0.0 /: ps) { (w, p) => w + (0 max parent.indexOf(p)) } / (ps.size max 1)
-          (v, weight)
+      child.map(v =>
+      {
+        val ps = if (top_down) graph.imm_preds(v) else graph.imm_succs(v)
+        val weight =
+          ps.foldLeft(0.0) { case (w, p) => w + (0 max parent.indexOf(p)) } / (ps.size max 1)
+        (v, weight)
       }).sortBy(_._2).map(_._1)
 
-    ((levels, count_crossings(graph, levels)) /:
-      (1 to (2 * options.int("graphview_iterations_minimize_crossings")))) {
-      case ((old_levels, old_crossings), iteration) =>
-        val top_down = (iteration % 2 == 1)
-        val new_levels =
-          if (top_down)
-            (List(old_levels.head) /: old_levels.tail)((tops, bot) =>
-              resort(tops.head, bot, top_down) :: tops).reverse
-          else {
-            val rev_old_levels = old_levels.reverse
-            (List(rev_old_levels.head) /: rev_old_levels.tail)((bots, top) =>
-              resort(bots.head, top, top_down) :: bots)
-          }
-        val new_crossings = count_crossings(graph, new_levels)
-        if (new_crossings < old_crossings)
-          (new_levels, new_crossings)
-        else
-          (old_levels, old_crossings)
-    }._1
+    (1 to (2 * options.int("graphview_iterations_minimize_crossings"))).
+      foldLeft((levels, count_crossings(graph, levels))) {
+        case ((old_levels, old_crossings), iteration) =>
+          val top_down = (iteration % 2 == 1)
+          val new_levels =
+            if (top_down) {
+              old_levels.tail.foldLeft(List(old_levels.head)) {
+                case (tops, bot) => resort(tops.head, bot, top_down) :: tops
+              }.reverse
+            }
+            else {
+              val rev_old_levels = old_levels.reverse
+              rev_old_levels.tail.foldLeft(List(rev_old_levels.head)) {
+                case (bots, top) => resort(bots.head, top, top_down) :: bots
+              }
+            }
+          val new_crossings = count_crossings(graph, new_levels)
+          if (new_crossings < old_crossings)
+            (new_levels, new_crossings)
+          else
+            (old_levels, old_crossings)
+      }._1
   }
 
   private def level_list(levels: Levels): List[Level] =
   {
-    val max_lev = (-1 /: levels) { case (m, (_, l)) => m max l }
+    val max_lev = levels.foldLeft(-1) { case (m, (_, l)) => m max l }
     val buckets = new Array[Level](max_lev + 1)
     for (l <- 0 to max_lev) { buckets(l) = Nil }
     for ((v, l) <- levels) { buckets(l) = v :: buckets(l) }
@@ -260,7 +266,7 @@
       }).sum / content.length).round.toDouble
 
     def move(graph: Graph, dx: Double): Graph =
-      if (dx == 0.0) graph else (graph /: content)(move_vertex(_, _, dx))
+      if (dx == 0.0) graph else content.foldLeft(graph)(move_vertex(_, _, dx))
 
     def combine(that: Region): Region = new Region(content ::: that.content)
   }
@@ -289,7 +295,7 @@
 
     def deflect(level: List[Region], top_down: Boolean, graph: Graph): (Graph, Boolean) =
     {
-      ((graph, false) /: level.indices) {
+      level.indices.foldLeft((graph, false)) {
         case ((graph, moved), i) =>
           val r = level(i)
           val d = r.deflection(graph, top_down)
@@ -307,22 +313,23 @@
 
     val initial_regions = levels.map(level => level.map(l => new Region(List(l))))
 
-    ((levels_graph, initial_regions, true) /:
-      (1 to (2 * options.int("graphview_iterations_pendulum")))) {
-      case ((graph, regions, moved), iteration) =>
-        val top_down = (iteration % 2 == 1)
-        if (moved) {
-          val (graph1, regions1, moved1) =
-            ((graph, List.empty[List[Region]], false) /:
-              (if (top_down) regions else regions.reverse)) { case ((graph, tops, moved), bot) =>
-                val bot1 = combine_regions(graph, top_down, bot)
-                val (graph1, moved1) = deflect(bot1, top_down, graph)
-                (graph1, bot1 :: tops, moved || moved1)
-            }
-          (graph1, regions1.reverse, moved1)
-        }
-        else (graph, regions, moved)
-    }._1
+    (1 to (2 * options.int("graphview_iterations_pendulum"))).
+      foldLeft((levels_graph, initial_regions, true)) {
+        case ((graph, regions, moved), iteration) =>
+          val top_down = (iteration % 2 == 1)
+          if (moved) {
+            val (graph1, regions1, moved1) =
+              (if (top_down) regions else regions.reverse).
+                foldLeft((graph, List.empty[List[Region]], false)) {
+                  case ((graph, tops, moved), bot) =>
+                    val bot1 = combine_regions(graph, top_down, bot)
+                    val (graph1, moved1) = deflect(bot1, top_down, graph)
+                    (graph1, bot1 :: tops, moved || moved1)
+                }
+            (graph1, regions1.reverse, moved1)
+          }
+          else (graph, regions, moved)
+      }._1
   }
 
 
@@ -346,18 +353,19 @@
   {
     val gap = metrics.gap
 
-    (graph /: (1 to (2 * options.int("graphview_iterations_rubberband")))) { case (graph, _) =>
-      (graph /: levels) { case (graph, level) =>
-        val m = level.length - 1
-        (graph /: level.iterator.zipWithIndex) {
-          case (g, (v, i)) =>
-            val d = force_weight(g, v)
-            if (d < 0.0 && (i == 0 || vertex_right(g, level(i - 1)) + gap < vertex_left(g, v) + d) ||
-                d > 0.0 && (i == m || vertex_left(g, level(i + 1)) - gap > vertex_right(g, v) + d))
-              move_vertex(g, v, d.round.toDouble)
-            else g
+    (1 to (2 * options.int("graphview_iterations_rubberband"))).foldLeft(graph) {
+      case (graph, _) =>
+        levels.foldLeft(graph) { case (graph, level) =>
+          val m = level.length - 1
+          level.iterator.zipWithIndex.foldLeft(graph) {
+            case (g, (v, i)) =>
+              val d = force_weight(g, v)
+              if (d < 0.0 && (i == 0 || vertex_right(g, level(i - 1)) + gap < vertex_left(g, v) + d) ||
+                  d > 0.0 && (i == m || vertex_left(g, level(i + 1)) - gap > vertex_right(g, v) + d))
+                move_vertex(g, v, d.round.toDouble)
+              else g
+          }
         }
-      }
     }
   }
 }
--- a/src/Tools/Graphview/metrics.scala	Wed Mar 03 22:48:46 2021 +0100
+++ b/src/Tools/Graphview/metrics.scala	Thu Mar 04 15:41:46 2021 +0100
@@ -46,7 +46,8 @@
   def dummy_size2: Double = (char_width / 2).ceil
 
   def node_width2(lines: List[String]): Double =
-    (((0.0 /: lines)({ case (w, s) => w max string_bounds(s).getWidth }) + 2 * char_width) / 2).ceil
+    ((lines.foldLeft(0.0)({ case (w, s) => w max string_bounds(s).getWidth }) + 2 * char_width) / 2)
+      .ceil
 
   def node_height2(num_lines: Int): Double =
     ((height.ceil * (num_lines max 1) + char_width) / 2).ceil
--- a/src/Tools/Graphview/model.scala	Wed Mar 03 22:48:46 2021 +0100
+++ b/src/Tools/Graphview/model.scala	Thu Mar 04 15:41:46 2021 +0100
@@ -54,7 +54,7 @@
     full_graph.keys_iterator.find(node => node.ident == ident)
 
   def make_visible_graph(): Graph_Display.Graph =
-    (full_graph /: Mutators()) {
+    Mutators().foldLeft(full_graph) {
       case (g, m) => if (!m.enabled) g else m.mutator.mutate(full_graph, g)
     }
 
@@ -64,9 +64,9 @@
   private def build_colors(): Unit =
   {
     _colors =
-      (Map.empty[Graph_Display.Node, Color] /: Colors()) {
+      Colors().foldLeft(Map.empty[Graph_Display.Node, Color]) {
         case (colors, m) =>
-          (colors /: m.mutator.mutate(full_graph, full_graph).keys_iterator) {
+          m.mutator.mutate(full_graph, full_graph).keys_iterator.foldLeft(colors) {
             case (colors, node) => colors + (node -> m.color)
           }
       }
--- a/src/Tools/Graphview/mutator.scala	Wed Mar 03 22:48:46 2021 +0100
+++ b/src/Tools/Graphview/mutator.scala	Thu Mar 04 15:41:46 2021 +0100
@@ -51,10 +51,11 @@
     extends Graph_Filter(
       name,
       description,
-      g => (g /: g.dest) {
+      g => g.dest.foldLeft(g) {
         case (graph, ((from, _), tos)) =>
-          (graph /: tos)((gr, to) =>
-            if (pred(gr, (from, to))) gr else gr.del_edge(from, to))
+          tos.foldLeft(graph) {
+            case (gr, to) => if (pred(gr, (from, to))) gr else gr.del_edge(from, to)
+          }
       })
 
   class Node_Family_Filter(
@@ -116,26 +117,24 @@
   {
     // Add Nodes
     val with_nodes =
-      (to /: keys)((graph, key) => graph.default_node(key, from.get_node(key)))
+      keys.foldLeft(to) { case (graph, key) => graph.default_node(key, from.get_node(key)) }
 
     // Add Edges
-    (with_nodes /: keys) {
-      (gv, key) => {
+    keys.foldLeft(with_nodes) {
+      case (gv, key) =>
         def add_edges(g: Graph_Display.Graph, keys: from.Keys, succs: Boolean) =
-          (g /: keys) {
-            (graph, end) => {
+          keys.foldLeft(g) {
+            case (graph, end) =>
               if (!graph.keys_iterator.contains(end)) graph
               else {
                 if (succs) graph.add_edge(key, end)
                 else graph.add_edge(end, key)
               }
-            }
           }
 
         add_edges(
           add_edges(gv, from.imm_preds(key), false),
           from.imm_succs(key), true)
-      }
     }
   }
 
--- a/src/Tools/Graphview/shapes.scala	Wed Mar 03 22:48:46 2021 +0100
+++ b/src/Tools/Graphview/shapes.scala	Thu Mar 04 15:41:46 2021 +0100
@@ -55,7 +55,7 @@
     gfx.setFont(metrics.font)
 
     val text_width =
-      (0.0 /: info.lines) { case (w, line) => w max metrics.string_bounds(line).getWidth }
+      info.lines.foldLeft(0.0) { case (w, line) => w max metrics.string_bounds(line).getWidth }
     val text_height =
       (info.lines.length max 1) * metrics.height.ceil
     val x = (s.getCenterX - text_width / 2).round.toInt
@@ -126,7 +126,7 @@
         val dy = coords(2).y - coords(0).y
 
         val (dx2, dy2) =
-          ((dx, dy) /: coords.sliding(3)) {
+          coords.sliding(3).foldLeft((dx, dy)) {
             case ((dx, dy), List(l, m, r)) =>
               val dx2 = r.x - l.x
               val dy2 = r.y - l.y
--- a/src/Tools/VSCode/src/preview_panel.scala	Wed Mar 03 22:48:46 2021 +0100
+++ b/src/Tools/VSCode/src/preview_panel.scala	Thu Mar 04 15:41:46 2021 +0100
@@ -24,22 +24,23 @@
     pending.change_result(map =>
     {
       val map1 =
-        (map /: map.iterator)({ case (m, (file, column)) =>
-          resources.get_model(file) match {
-            case Some(model) =>
-              val snapshot = model.snapshot()
-              if (snapshot.is_outdated) m
-              else {
-                val html_context = Presentation.html_context()
-                val document =
-                  Presentation.html_document(
-                    resources, snapshot, html_context, Presentation.elements2)
-                channel.write(LSP.Preview_Response(file, column, document.title, document.content))
-                m - file
-              }
-            case None => m - file
-          }
-        })
+        map.iterator.foldLeft(map) {
+          case (m, (file, column)) =>
+            resources.get_model(file) match {
+              case Some(model) =>
+                val snapshot = model.snapshot()
+                if (snapshot.is_outdated) m
+                else {
+                  val html_context = Presentation.html_context()
+                  val document =
+                    Presentation.html_document(
+                      resources, snapshot, html_context, Presentation.elements2)
+                  channel.write(LSP.Preview_Response(file, column, document.title, document.content))
+                  m - file
+                }
+              case None => m - file
+            }
+        }
       (map1.nonEmpty, map1)
     })
   }
--- a/src/Tools/VSCode/src/vscode_rendering.scala	Wed Mar 03 22:48:46 2021 +0100
+++ b/src/Tools/VSCode/src/vscode_rendering.scala	Thu Mar 04 15:41:46 2021 +0100
@@ -23,7 +23,7 @@
     colors: List[Text.Info[Rendering.Color.Value]]): List[VSCode_Model.Decoration] =
   {
     val color_ranges =
-      (Map.empty[Rendering.Color.Value, List[Text.Range]] /: colors) {
+      colors.foldLeft(Map.empty[Rendering.Color.Value, List[Text.Range]]) {
         case (m, Text.Info(range, c)) => m + (c -> (range :: m.getOrElse(c, Nil)))
       }
     types.toList.map(c =>
@@ -324,7 +324,7 @@
                 Text.Info(entry_range, (entry, model)) <- bibtex_entries_iterator()
                 if entry == name
               } yield Line.Node_Range(model.node_name.node, model.content.doc.range(entry_range))
-            if (iterator.isEmpty) None else Some((links /: iterator)(_ :+ _))
+            if (iterator.isEmpty) None else Some(iterator.foldLeft(links)(_ :+ _))
 
           case _ => None
         }) match { case Text.Info(_, links) :: _ => links.reverse case _ => Nil }
--- 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
--- a/src/Tools/jEdit/src/isabelle_sidekick.scala	Wed Mar 03 22:48:46 2021 +0100
+++ b/src/Tools/jEdit/src/isabelle_sidekick.scala	Thu Mar 04 15:41:46 2021 +0100
@@ -121,18 +121,19 @@
       offset: Text.Offset,
       documents: List[Document_Structure.Document]): Unit =
     {
-      documents.foldLeft(offset) { case (i, document) =>
-        document match {
-          case Document_Structure.Block(name, text, body) =>
-            val range = Text.Range(i, i + document.length)
-            val node =
-              new DefaultMutableTreeNode(
-                new Isabelle_Sidekick.Keyword_Asset(name, Library.first_line(text), range))
-            parent.add(node)
-            make_tree(node, i, body)
-          case _ =>
-        }
-        i + document.length
+      documents.foldLeft(offset) {
+        case (i, document) =>
+          document match {
+            case Document_Structure.Block(name, text, body) =>
+              val range = Text.Range(i, i + document.length)
+              val node =
+                new DefaultMutableTreeNode(
+                  new Isabelle_Sidekick.Keyword_Asset(name, Library.first_line(text), range))
+              parent.add(node)
+              make_tree(node, i, body)
+            case _ =>
+          }
+          i + document.length
       }
     }
 
--- a/src/Tools/jEdit/src/pretty_tooltip.scala	Wed Mar 03 22:48:46 2021 +0100
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Thu Mar 04 15:41:46 2021 +0100
@@ -267,7 +267,7 @@
       val h = painter.getLineHeight * lines + geometry.deco_height
       val margin1 =
         if (h <= h_max) {
-          split_lines(XML.content(formatted)).foldLeft(0.0)({ case (m, line) => m max metric(line) })
+          split_lines(XML.content(formatted)).foldLeft(0.0) { case (m, line) => m max metric(line) }
         }
         else margin
       val w = (metric.unit * (margin1 + metric.average)).round.toInt + geometry.deco_width
--- a/src/Tools/jEdit/src/text_structure.scala	Wed Mar 03 22:48:46 2021 +0100
+++ b/src/Tools/jEdit/src/text_structure.scala	Thu Mar 04 15:41:46 2021 +0100
@@ -130,11 +130,12 @@
               }).collectFirst({ case (i, true) => i }).getOrElse(0)
 
           def indent_brackets: Int =
-            prev_line_span.foldLeft(0)(
-              { case (i, tok) =>
-                  if (tok.is_open_bracket) i + indent_size
-                  else if (tok.is_close_bracket) i - indent_size
-                  else i })
+            prev_line_span.foldLeft(0) {
+              case (i, tok) =>
+                if (tok.is_open_bracket) i + indent_size
+                else if (tok.is_close_bracket) i - indent_size
+                else i
+            }
 
           def indent_extra: Int =
             if (prev_span.exists(keywords.is_quasi_command)) indent_size
--- a/src/Tools/jEdit/src/theories_dockable.scala	Wed Mar 03 22:48:46 2021 +0100
+++ b/src/Tools/jEdit/src/theories_dockable.scala	Thu Mar 04 15:41:46 2021 +0100
@@ -159,11 +159,12 @@
                 (node_status.failed, PIDE.options.color_value("error_color"))
               ).filter(_._1 > 0)
 
-            segments.foldLeft(size.width - 2)({ case (last, (n, color)) =>
-              val w = (n * ((size.width - 4) - segments.length) / node_status.total) max 4
-              paint_segment(last - w, w, color)
-              last - w - 1
-            })
+            segments.foldLeft(size.width - 2) {
+              case (last, (n, color)) =>
+                val w = (n * ((size.width - 4) - segments.length) / node_status.total) max 4
+                paint_segment(last - w, w, color)
+                last - w - 1
+              }
 
           case None =>
             paint_segment(0, size.width, PIDE.options.color_value("unprocessed1_color"))
--- a/src/Tools/jEdit/src/timing_dockable.scala	Wed Mar 03 22:48:46 2021 +0100
+++ b/src/Tools/jEdit/src/timing_dockable.scala	Thu Mar 04 15:41:46 2021 +0100
@@ -186,9 +186,8 @@
       (restriction match {
         case Some(names) => names.iterator.map(name => (name, snapshot.get_node(name)))
         case None => snapshot.version.nodes.iterator
-      })
-      .foldLeft(nodes_timing)(
-        { case (timing1, (name, node)) =>
+      }).foldLeft(nodes_timing) {
+          case (timing1, (name, node)) =>
             if (PIDE.resources.session_base.loaded_theory(name)) timing1
             else {
               val node_timing =
@@ -196,7 +195,7 @@
                   snapshot.state, snapshot.version, node.commands, threshold = timing_threshold)
               timing1 + (name -> node_timing)
             }
-        })
+        }
     nodes_timing = nodes_timing1
 
     val entries = make_entries()