merged
authordesharna
Fri, 05 Mar 2021 08:22:34 +0100
changeset 73625 39826af584bf
parent 73624 96ef620c8b1e (current diff)
parent 73620 3bb9df8900fd (diff)
child 73626 10f5f5b880f4
merged
--- a/etc/settings	Thu Mar 04 18:38:56 2021 +0100
+++ b/etc/settings	Fri Mar 05 08:22:34 2021 +0100
@@ -16,7 +16,7 @@
 
 ISABELLE_TOOL_JAVA_OPTIONS="-Djava.awt.headless=true -Xms512m -Xmx4g -Xss16m"
 
-ISABELLE_SCALAC_OPTIONS="-encoding UTF-8 -nowarn -target:11 -J-Xms512m -J-Xmx4g -J-Xss16m"
+ISABELLE_SCALAC_OPTIONS="-encoding UTF-8 -Wconf:cat=other-match-analysis:silent -feature -deprecation -target:11 -J-Xms512m -J-Xmx4g -J-Xss16m"
 
 classpath "$ISABELLE_HOME/lib/classes/Pure.jar"
 
--- a/src/HOL/Analysis/Affine.thy	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/HOL/Analysis/Affine.thy	Fri Mar 05 08:22:34 2021 +0100
@@ -1612,26 +1612,29 @@
   assumes "\<not> affine_dependent s" "t \<subseteq> s" "u \<subseteq> s" "t \<inter> u = {}"
     shows "(affine hull t) \<inter> (affine hull u) = {}"
 proof -
-  have "finite s" using assms by (simp add: aff_independent_finite)
-  then have "finite t" "finite u" using assms finite_subset by blast+
-  { fix y
-    assume yt: "y \<in> affine hull t" and yu: "y \<in> affine hull u"
-    then obtain a b
-           where a1 [simp]: "sum a t = 1" and [simp]: "sum (\<lambda>v. a v *\<^sub>R v) t = y"
-             and [simp]: "sum b u = 1" "sum (\<lambda>v. b v *\<^sub>R v) u = y"
+  from assms(1) have "finite s"
+    by (simp add: aff_independent_finite)
+  with assms(2,3) have "finite t" "finite u"
+    by (blast intro: finite_subset)+
+  have False if "y \<in> affine hull t" and "y \<in> affine hull u" for y
+  proof -
+    from that obtain a b
+      where a1 [simp]: "sum a t = 1"
+        and [simp]: "sum (\<lambda>v. a v *\<^sub>R v) t = y"
+        and [simp]: "sum b u = 1" "sum (\<lambda>v. b v *\<^sub>R v) u = y"
       by (auto simp: affine_hull_finite \<open>finite t\<close> \<open>finite u\<close>)
     define c where "c x = (if x \<in> t then a x else if x \<in> u then -(b x) else 0)" for x
-    have [simp]: "s \<inter> t = t" "s \<inter> - t \<inter> u = u" using assms by auto
+    from assms(2,3,4) have [simp]: "s \<inter> t = t" "s \<inter> - t \<inter> u = u"
+      by auto
     have "sum c s = 0"
       by (simp add: c_def comm_monoid_add_class.sum.If_cases \<open>finite s\<close> sum_negf)
     moreover have "\<not> (\<forall>v\<in>s. c v = 0)"
       by (metis (no_types) IntD1 \<open>s \<inter> t = t\<close> a1 c_def sum.neutral zero_neq_one)
     moreover have "(\<Sum>v\<in>s. c v *\<^sub>R v) = 0"
-      by (simp add: c_def if_smult sum_negf
-             comm_monoid_add_class.sum.If_cases \<open>finite s\<close>)
-    ultimately have False
-      using assms \<open>finite s\<close> by (auto simp: affine_dependent_explicit)
-  }
+      by (simp add: c_def if_smult sum_negf comm_monoid_add_class.sum.If_cases \<open>finite s\<close>)
+    ultimately show ?thesis
+      using assms(1) \<open>finite s\<close> by (auto simp: affine_dependent_explicit)
+  qed
   then show ?thesis by blast
 qed
 
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Fri Mar 05 08:22:34 2021 +0100
@@ -3729,7 +3729,6 @@
     then have eba8: "(e * (b-a)) / 8 > 0"
       using ab by (auto simp add: field_simps)
     note derf_exp = derf[unfolded has_vector_derivative_def has_derivative_at_alt, THEN conjunct2, rule_format]
-    thm derf_exp
     have bounded: "\<And>x. x \<in> {a<..<b} \<Longrightarrow> bounded_linear (\<lambda>u. u *\<^sub>R f' x)"
       by (simp add: bounded_linear_scaleR_left)
     have "\<forall>x \<in> box a b. \<exists>d>0. \<forall>y. norm (y-x) < d \<longrightarrow> norm (f y - f x - (y-x) *\<^sub>R f' x) \<le> e/2 * norm (y-x)"
--- a/src/HOL/Tools/Nitpick/kodkod.scala	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/HOL/Tools/Nitpick/kodkod.scala	Fri Mar 05 08:22:34 2021 +0100
@@ -96,7 +96,7 @@
     /* main */
 
     try {
-      val lexer = new KodkodiLexer(new ANTLRInputStream(Bytes(source).stream))
+      val lexer = new KodkodiLexer(new ANTLRInputStream(Bytes(source).stream()))
       val parser =
         KodkodiParser.create(context, executor,
           false, solve_all, prove, max_solutions, cleanup_inst, lexer)
@@ -114,7 +114,7 @@
       try { parser.problems() }
       catch { case exn: RecognitionException => parser.reportError(exn) }
 
-      timeout_request.foreach(_.cancel)
+      timeout_request.foreach(_.cancel())
 
       if (parser.getTokenStream.LA(1) != KodkodiParser.EOF) {
         context.error("Error: trailing tokens")
--- a/src/Pure/Admin/afp.scala	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/Admin/afp.scala	Fri Mar 05 08:22:34 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	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/Admin/build_csdp.scala	Fri Mar 05 08:22:34 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	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/Admin/build_history.scala	Fri Mar 05 08:22:34 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	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/Admin/build_status.scala	Fri Mar 05 08:22:34 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	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/Admin/ci_profile.scala	Fri Mar 05 08:22:34 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	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Fri Mar 05 08:22:34 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/Concurrent/delay.scala	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/Concurrent/delay.scala	Fri Mar 05 08:22:34 2021 +0100
@@ -37,7 +37,7 @@
   {
     val new_run =
       running match {
-        case Some(request) => if (first) false else { request.cancel; true }
+        case Some(request) => if (first) false else { request.cancel(); true }
         case None => true
       }
     if (new_run)
@@ -47,7 +47,7 @@
   def revoke(): Unit = synchronized
   {
     running match {
-      case Some(request) => request.cancel; running = None
+      case Some(request) => request.cancel(); running = None
       case None =>
     }
   }
@@ -57,7 +57,7 @@
     running match {
       case Some(request) =>
         val alt_time = Time.now() + alt_delay
-        if (request.time < alt_time && request.cancel) {
+        if (request.time < alt_time && request.cancel()) {
           running = Some(Event_Timer.request(alt_time)(run))
         }
       case None =>
--- a/src/Pure/Concurrent/event_timer.scala	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/Concurrent/event_timer.scala	Fri Mar 05 08:22:34 2021 +0100
@@ -19,7 +19,7 @@
 
   final class Request private[Event_Timer](val time: Time, val repeat: Option[Time], task: TimerTask)
   {
-    def cancel: Boolean = task.cancel
+    def cancel(): Boolean = task.cancel()
   }
 
   def request(time: Time, repeat: Option[Time] = None)(event: => Unit): Request =
--- a/src/Pure/Concurrent/future.scala	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/Concurrent/future.scala	Fri Mar 05 08:22:34 2021 +0100
@@ -38,7 +38,7 @@
   def join_result: Exn.Result[A]
   def join: A = Exn.release(join_result)
   def map[B](f: A => B): Future[B] = Future.fork { f(join) }
-  def cancel: Unit
+  def cancel(): Unit
 
   override def toString: String =
     peek match {
@@ -61,7 +61,7 @@
 {
   val peek: Option[Exn.Result[A]] = Some(Exn.Res(x))
   def join_result: Exn.Result[A] = peek.get
-  def cancel: Unit = {}
+  def cancel(): Unit = {}
 }
 
 
@@ -93,7 +93,7 @@
     if (do_run) {
       val result = Exn.capture(body)
       status.change(_ => Terminated)
-      status.change(_ => Finished(if (Thread.interrupted) Exn.Exn(Exn.Interrupt()) else result))
+      status.change(_ => Finished(if (Thread.interrupted()) Exn.Exn(Exn.Interrupt()) else result))
     }
   }
   private val task = Isabelle_Thread.pool.submit(new Callable[Unit] { def call = try_run() })
@@ -107,11 +107,11 @@
     }
   }
 
-  def cancel =
+  def cancel(): Unit =
   {
     status.change {
       case Ready => task.cancel(false); Finished(Exn.Exn(Exn.Interrupt()))
-      case st @ Running(thread) => thread.interrupt; st
+      case st @ Running(thread) => thread.interrupt(); st
       case st => st
     }
   }
@@ -133,7 +133,7 @@
 
   def fulfill(x: A): Unit = fulfill_result(Exn.Res(x))
 
-  def cancel: Unit =
+  def cancel(): Unit =
     state.change(st => if (st.isEmpty) Some(Exn.Exn(Exn.Interrupt())) else st)
 }
 
@@ -157,5 +157,5 @@
 
   def peek: Option[Exn.Result[A]] = result.peek
   def join_result: Exn.Result[A] = result.join_result
-  def cancel: Unit = thread.interrupt
+  def cancel(): Unit = thread.interrupt()
 }
--- a/src/Pure/Concurrent/isabelle_thread.scala	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/Concurrent/isabelle_thread.scala	Fri Mar 05 08:22:34 2021 +0100
@@ -174,7 +174,7 @@
   // non-synchronized, only changed on self-thread
   @volatile private var handler = Isabelle_Thread.Interrupt_Handler.interruptible
 
-  override def interrupt: Unit = handler(thread)
+  override def interrupt(): Unit = handler(thread)
 
   def interrupt_handler[A](new_handler: Isabelle_Thread.Interrupt_Handler)(body: => A): A =
     if (new_handler == null) body
@@ -184,12 +184,12 @@
       val old_handler = handler
       handler = new_handler
       try {
-        if (clear_interrupt) interrupt
+        if (clear_interrupt) interrupt()
         body
       }
       finally {
         handler = old_handler
-        if (clear_interrupt) interrupt
+        if (clear_interrupt) interrupt()
       }
     }
 }
--- a/src/Pure/Concurrent/par_list.scala	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/Concurrent/par_list.scala	Fri Mar 05 08:22:34 2021 +0100
@@ -19,7 +19,7 @@
         state.change { case (futures, canceled) =>
           if (!canceled) {
             for ((future, i) <- futures.iterator.zipWithIndex if i != self)
-              future.cancel
+              future.cancel()
           }
           (futures, true)
         }
--- a/src/Pure/GUI/gui.scala	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/GUI/gui.scala	Fri Mar 05 08:22:34 2021 +0100
@@ -22,10 +22,10 @@
 
   def init_laf(): Unit = com.formdev.flatlaf.FlatLightLaf.install()
 
-  def current_laf(): String = UIManager.getLookAndFeel.getClass.getName()
+  def current_laf: String = UIManager.getLookAndFeel.getClass.getName()
 
-  def is_macos_laf(): Boolean =
-    Platform.is_macos && UIManager.getSystemLookAndFeelClassName() == current_laf()
+  def is_macos_laf: Boolean =
+    Platform.is_macos && UIManager.getSystemLookAndFeelClassName() == current_laf
 
   class Look_And_Feel(laf: LookAndFeel) extends Isabelle_System.Service
   {
--- a/src/Pure/General/completion.scala	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/General/completion.scala	Fri Mar 05 08:22:34 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/exn.scala	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/General/exn.scala	Fri Mar 05 08:22:34 2021 +0100
@@ -102,9 +102,9 @@
     def apply(): Throwable = new InterruptedException("Interrupt")
     def unapply(exn: Throwable): Boolean = is_interrupt(exn)
 
-    def dispose(): Unit = Thread.interrupted
-    def expose(): Unit = if (Thread.interrupted) throw apply()
-    def impose(): Unit = Thread.currentThread.interrupt
+    def dispose(): Unit = Thread.interrupted()
+    def expose(): Unit = if (Thread.interrupted()) throw apply()
+    def impose(): Unit = Thread.currentThread.interrupt()
 
     val return_code = 130
   }
--- a/src/Pure/General/file.scala	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/General/file.scala	Fri Mar 05 08:22:34 2021 +0100
@@ -199,7 +199,7 @@
     val output = new StringBuilder(100)
     var c = -1
     while ({ c = reader.read; c != -1 }) output += c.toChar
-    reader.close
+    reader.close()
     output.toString
   }
 
@@ -233,7 +233,7 @@
       progress(line.get)
       result += line.get
     }
-    reader.close
+    reader.close()
     result.toList
   }
 
--- a/src/Pure/General/file_watcher.scala	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/General/file_watcher.scala	Fri Mar 05 08:22:34 2021 +0100
@@ -72,14 +72,14 @@
         st.dirs.get(dir) match {
           case None => st
           case Some(key) =>
-            key.cancel
+            key.cancel()
             st.copy(dirs = st.dirs - dir)
         })
 
     override def purge(retain: Set[JFile]): Unit =
       state.change(st =>
         st.copy(dirs = st.dirs --
-          (for ((dir, key) <- st.dirs.iterator if !retain(dir)) yield { key.cancel; dir })))
+          (for ((dir, key) <- st.dirs.iterator if !retain(dir)) yield { key.cancel(); dir })))
 
 
     /* changed directory entries */
@@ -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)
@@ -127,9 +127,9 @@
 
     override def shutdown(): Unit =
     {
-      watcher_thread.interrupt
+      watcher_thread.interrupt()
       watcher_thread.join
-      delay_changed.revoke
+      delay_changed.revoke()
     }
   }
 }
--- a/src/Pure/General/graph.scala	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/General/graph.scala	Fri Mar 05 08:22:34 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,8 +168,8 @@
       if (r_set(x)) reached
       else {
         val (rs1, r_set1) =
-          if (rev) ((rs, r_set + x) /: next(x))({ case (b, a) => reach(a, b) })
-          else (next(x) :\ (rs, r_set + x))(reach)
+          if (rev) next(x).foldLeft((rs, r_set + x)) { case (b, a) => reach(a, b) }
+          else next(x).foldRight((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	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/General/graph_display.scala	Fri Mar 05 08:22:34 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/http.scala	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/General/http.scala	Fri Mar 05 08:22:34 2021 +0100
@@ -109,8 +109,8 @@
     def += (handler: Handler): Unit = http_server.createContext(handler.root, handler.handler)
     def -= (handler: Handler): Unit = http_server.removeContext(handler.root)
 
-    def start: Unit = http_server.start
-    def stop: Unit = http_server.stop(0)
+    def start(): Unit = http_server.start
+    def stop(): Unit = http_server.stop(0)
 
     def address: InetSocketAddress = http_server.getAddress
     def url: String = "http://" + address.getHostName + ":" + address.getPort
--- a/src/Pure/General/linear_set.scala	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/General/linear_set.scala	Fri Mar 05 08:22:34 2021 +0100
@@ -18,7 +18,8 @@
   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.iterator.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 +84,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/mailman.scala	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/General/mailman.scala	Fri Mar 05 08:22:34 2021 +0100
@@ -55,7 +55,7 @@
               Some(path)
             }
           }
-          finally { connection.getInputStream.close }
+          finally { connection.getInputStream.close() }
         })
     }
   }
--- a/src/Pure/General/mercurial.scala	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/General/mercurial.scala	Fri Mar 05 08:22:34 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	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/General/multi_map.scala	Fri Mar 05 08:22:34 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.iterator.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,8 +63,8 @@
     if (this eq other) this
     else if (isEmpty) other
     else
-      (this.asInstanceOf[Multi_Map[A, B1]] /: other.rep.iterator) {
-        case (m1, (a, bs)) => (bs :\ m1) { case (b, m2) => m2.insert(a, b) }
+      other.rep.iterator.foldLeft(this.asInstanceOf[Multi_Map[A, B1]]) {
+        case (m1, (a, bs)) => bs.foldRight(m1) { case (b, m2) => m2.insert(a, b) }
       }
 
 
--- a/src/Pure/General/path.scala	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/General/path.scala	Fri Mar 05 08:22:34 2021 +0100
@@ -54,7 +54,7 @@
     }
 
   private def norm_elems(elems: List[Elem]): List[Elem] =
-    (elems :\ (Nil: List[Elem]))(apply_elem)
+    elems.foldRight(List.empty[Elem])(apply_elem)
 
   private def implode_elem(elem: Elem, short: Boolean): String =
     elem match {
@@ -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) {
@@ -174,7 +174,7 @@
   def is_basic: Boolean = elems match { case List(Path.Basic(_)) => true case _ => false }
   def starts_basic: Boolean = elems.nonEmpty && elems.last.isInstanceOf[Path.Basic]
 
-  def +(other: Path): Path = new Path((other.elems :\ elems)(Path.apply_elem))
+  def +(other: Path): Path = new Path(other.elems.foldRight(elems)(Path.apply_elem))
 
 
   /* implode */
--- a/src/Pure/General/pretty.scala	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/General/pretty.scala	Fri Mar 05 08:22:34 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	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/General/scan.scala	Fri Mar 05 08:22:34 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,8 @@
         new Lexicon(extend(rep, 0))
       }
 
-    def ++ (elems: IterableOnce[String]): Lexicon = (this /: elems)(_ + _)
+    def ++ (elems: IterableOnce[String]): Lexicon =
+      elems.iterator.foldLeft(this)(_ + _)
 
     def ++ (other: Lexicon): Lexicon =
       if (this eq other) this
@@ -478,7 +479,7 @@
       def pos: InputPosition = new OffsetPosition(source, offset)
       def atEnd: Boolean = !seq.isDefinedAt(offset)
       override def drop(n: Int): Paged_Reader = new Paged_Reader(offset + n)
-      def close: Unit = buffered_stream.close
+      def close(): Unit = buffered_stream.close()
     }
     new Paged_Reader(0)
   }
--- a/src/Pure/General/sql.scala	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/General/sql.scala	Fri Mar 05 08:22:34 2021 +0100
@@ -253,7 +253,7 @@
     def execute(): Boolean = rep.execute()
     def execute_query(): Result = new Result(this, rep.executeQuery())
 
-    def close(): Unit = rep.close
+    def close(): Unit = rep.close()
   }
 
 
@@ -322,7 +322,7 @@
 
     def connection: Connection
 
-    def close(): Unit = connection.close
+    def close(): Unit = connection.close()
 
     def transaction[A](body: => A): A =
     {
@@ -483,7 +483,7 @@
       val connection = DriverManager.getConnection(url, user, password)
       new Database(name, connection, port_forwarding)
     }
-    catch { case exn: Throwable => port_forwarding.foreach(_.close); throw exn }
+    catch { case exn: Throwable => port_forwarding.foreach(_.close()); throw exn }
   }
 
   class Database private[PostgreSQL](
@@ -509,6 +509,6 @@
       table.insert_cmd("INSERT",
         sql = sql + (if (sql == "") "" else " ") + "ON CONFLICT DO NOTHING")
 
-    override def close(): Unit = { super.close; port_forwarding.foreach(_.close) }
+    override def close(): Unit = { super.close(); port_forwarding.foreach(_.close()) }
   }
 }
--- a/src/Pure/General/ssh.scala	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/General/ssh.scala	Fri Mar 05 08:22:34 2021 +0100
@@ -141,15 +141,15 @@
 
         val fw =
           try { proxy.port_forwarding(remote_host = connect_host, remote_port = make_port(port)) }
-          catch { case exn: Throwable => proxy.close; throw exn }
+          catch { case exn: Throwable => proxy.close(); throw exn }
 
         try {
           connect_session(host = fw.local_host, port = fw.local_port,
             host_key_permissive = permissive,
             nominal_host = host, nominal_user = user, user = user,
-            on_close = () => { fw.close; proxy.close })
+            on_close = () => { fw.close(); proxy.close() })
         }
-        catch { case exn: Throwable => fw.close; proxy.close; throw exn }
+        catch { case exn: Throwable => fw.close(); proxy.close(); throw exn }
       }
     }
   }
@@ -259,7 +259,7 @@
       progress_stderr: String => Unit = (_: String) => (),
       strict: Boolean = true): Process_Result =
     {
-      stdin.close
+      stdin.close()
 
       def read_lines(stream: InputStream, progress: String => Unit): List[String] =
       {
@@ -293,7 +293,7 @@
 
       def terminate(): Unit =
       {
-        close
+        close()
         out_lines.join
         err_lines.join
         exit_status.join
@@ -303,7 +303,7 @@
         try { exit_status.join }
         catch { case Exn.Interrupt() => terminate(); Exn.Interrupt.return_code }
 
-      close
+      close()
       if (strict && rc == Exn.Interrupt.return_code) throw Exn.Interrupt()
 
       Process_Result(rc, out_lines.join, err_lines.join)
--- a/src/Pure/General/symbol.scala	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/General/symbol.scala	Fri Mar 05 08:22:34 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/General/url.scala	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/General/url.scala	Fri Mar 05 08:22:34 2021 +0100
@@ -43,7 +43,7 @@
     catch { case ERROR(_) => false }
 
   def is_readable(name: String): Boolean =
-    try { Url(name).openStream.close; true }
+    try { Url(name).openStream.close(); true }
     catch { case ERROR(_) => false }
 
 
--- a/src/Pure/Isar/document_structure.scala	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/Isar/document_structure.scala	Fri Mar 05 08:22:34 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	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/Isar/keyword.scala	Fri Mar 05 08:22:34 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	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/Isar/line_structure.scala	Fri Mar 05 08:22:34 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	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/Isar/outer_syntax.scala	Fri Mar 05 08:22:34 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))
@@ -188,8 +189,8 @@
 
     def flush(): Unit =
     {
-      if (content.nonEmpty) { ship(content.toList); content.clear }
-      if (ignored.nonEmpty) { ship(ignored.toList); ignored.clear }
+      if (content.nonEmpty) { ship(content.toList); content.clear() }
+      if (ignored.nonEmpty) { ship(ignored.toList); ignored.clear() }
     }
 
     for (tok <- toks) {
@@ -198,7 +199,7 @@
         tok.is_command &&
           (!content.exists(keywords.is_before_command) || content.exists(_.is_command)))
       { flush(); content += tok }
-      else { content ++= ignored; ignored.clear; content += tok }
+      else { content ++= ignored; ignored.clear(); content += tok }
     }
     flush()
 
--- a/src/Pure/ML/ml_console.scala	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/ML/ml_console.scala	Fri Mar 05 08:22:34 2021 +0100
@@ -74,7 +74,7 @@
             else Some(Sessions.base_info(
               options, logic, dirs = dirs, include_sessions = include_sessions).check.base))
 
-      POSIX_Interrupt.handler { process.interrupt } {
+      POSIX_Interrupt.handler { process.interrupt() } {
         new TTY_Loop(process.stdin, process.stdout).join
         val rc = process.join
         if (rc != 0) sys.exit(rc)
--- a/src/Pure/ML/ml_statistics.scala	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/ML/ml_statistics.scala	Fri Mar 05 08:22:34 2021 +0100
@@ -93,7 +93,7 @@
     override def exit(): Unit = synchronized
     {
       session = null
-      monitoring.cancel
+      monitoring.cancel()
     }
 
     private def consume(props: Properties.T): Unit = synchronized
@@ -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	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/PIDE/command.scala	Fri Mar 05 08:22:34 2021 +0100
@@ -56,8 +56,10 @@
   {
     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.iterator.foldLeft(empty)(_ + _)
+    def merge(args: IterableOnce[Results]): Results =
+      args.iterator.foldLeft(empty)(_ ++ _)
   }
 
   final class Results private(private val rep: SortedMap[Long, XML.Elem])
@@ -74,7 +76,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 +94,8 @@
   {
     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.iterator.foldLeft(empty)(_ ++ _)
   }
 
   final class Exports private(private val rep: SortedMap[Long, Export.Entry])
@@ -107,7 +110,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 +137,10 @@
     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.iterator.foldLeft(empty)(_ + _)
+    def merge(args: IterableOnce[Markups]): Markups =
+      args.iterator.foldLeft(empty)(_ ++ _)
   }
 
   final class Markups private(private val rep: Map[Markup_Index, Markup_Tree])
@@ -157,7 +162,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 +300,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 +349,7 @@
                   }
                 case _ => bad(); state
               }
-            })
+          }
 
         case XML.Elem(Markup(name, props), body) =>
           props match {
@@ -512,7 +519,7 @@
     val init_results: Command.Results,
     val init_markups: Command.Markups)
 {
-  override def toString: String = id + "/" + span.kind.toString
+  override def toString: String = id.toString + "/" + span.kind.toString
 
 
   /* classification */
@@ -562,7 +569,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	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/PIDE/command_span.scala	Fri Mar 05 08:22:34 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	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/PIDE/document.scala	Fri Mar 05 08:22:34 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((List.empty[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	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/PIDE/document_status.scala	Fri Mar 05 08:22:34 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	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/PIDE/headless.scala	Fri Mar 05 08:22:34 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 =
@@ -336,7 +337,7 @@
                         domain = Some(domain), trim = changed.assignment)
 
                     if (nodes_status_delay >= Time.zero && nodes_status_changed) {
-                      delay_nodes_status.invoke
+                      delay_nodes_status.invoke()
                     }
 
                     val theory_progress =
@@ -356,8 +357,8 @@
 
               if (commit.isDefined && commit_cleanup_delay > Time.zero) {
                 if (use_theories_state.value.finished_result)
-                  delay_commit_clean.revoke
-                else delay_commit_clean.invoke
+                  delay_commit_clean.revoke()
+                else delay_commit_clean.invoke()
               }
             }
         }
@@ -367,7 +368,7 @@
         session.commands_changed += consumer
         check_state()
         use_theories_state.guarded_access(_.join_result)
-        check_progress.cancel
+        check_progress.cancel()
       }
       finally {
         session.commands_changed -= consumer
@@ -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 =
       {
@@ -573,7 +575,7 @@
 
       progress.echo("Starting session " + session_base_info.session + " ...")
       Isabelle_Process(session, options, session_base_info.sessions_structure, store,
-        logic = session_base_info.session, modes = print_mode).await_startup
+        logic = session_base_info.session, modes = print_mode).await_startup()
 
       session
     }
--- a/src/Pure/PIDE/line.scala	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/PIDE/line.scala	Fri Mar 05 08:22:34 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.scala	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/PIDE/markup.scala	Fri Mar 05 08:22:34 2021 +0100
@@ -733,7 +733,7 @@
 
   def update_properties(more_props: Properties.T): Markup =
     if (more_props.isEmpty) this
-    else Markup(name, (more_props :\ properties) { case (p, ps) => Properties.put(ps, p) })
+    else Markup(name, more_props.foldRight(properties) { case (p, ps) => Properties.put(ps, p) })
 
   def + (entry: Properties.Entry): Markup =
     Markup(name, Properties.put(properties, entry))
--- a/src/Pure/PIDE/markup_tree.scala	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/PIDE/markup_tree.scala	Fri Mar 05 08:22:34 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, List.empty[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, List.empty[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	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/PIDE/protocol_handlers.scala	Fri Mar 05 08:22:34 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	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/PIDE/prover.scala	Fri Mar 05 08:22:34 2021 +0100
@@ -106,7 +106,7 @@
 
   private def terminate_process(): Unit =
   {
-    try { process.terminate }
+    try { process.terminate() }
     catch {
       case exn @ ERROR(_) => system_output("Failed to terminate prover process: " + exn.getMessage)
     }
@@ -184,7 +184,7 @@
 
   private var command_input: Option[Consumer_Thread[List[Bytes]]] = None
 
-  private def command_input_close(): Unit = command_input.foreach(_.shutdown)
+  private def command_input_close(): Unit = command_input.foreach(_.shutdown())
 
   private def command_input_init(raw_stream: OutputStream): Unit =
   {
@@ -204,7 +204,7 @@
                 }
                 catch { case e: IOException => system_output(name + ": " + e.getMessage); false }
             },
-          finish = { case () => stream.close; system_output(name + " terminated") }
+          finish = { case () => stream.close(); system_output(name + " terminated") }
         )
       )
   }
@@ -233,10 +233,10 @@
           }
           if (result.nonEmpty) {
             output(markup, Nil, List(XML.Text(Symbol.decode(result.toString))))
-            result.clear
+            result.clear()
           }
           else {
-            reader.close
+            reader.close()
             finished = true
           }
           //}}}
@@ -333,7 +333,7 @@
         case e: IOException => system_output("Cannot read message:\n" + e.getMessage)
         case e: Protocol_Error => system_output("Malformed message:\n" + e.getMessage)
       }
-      stream.close
+      stream.close()
 
       system_output(name + " terminated")
     }
@@ -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	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/PIDE/rendering.scala	Fri Mar 05 08:22:34 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	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/PIDE/resources.scala	Fri Mar 05 08:22:34 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/session.scala	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/PIDE/session.scala	Fri Mar 05 08:22:34 2021 +0100
@@ -624,7 +624,7 @@
             delay_prune.revoke()
             if (prover.defined) {
               global_state.change(_ => Document.State.init)
-              prover.get.terminate
+              prover.get.terminate()
             }
 
           case Get_State(promise) =>
--- a/src/Pure/PIDE/xml.scala	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/PIDE/xml.scala	Fri Mar 05 08:22:34 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/ROOT.ML	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/ROOT.ML	Fri Mar 05 08:22:34 2021 +0100
@@ -355,4 +355,3 @@
 ML_file "Tools/jedit.ML";
 ML_file "Tools/ghc.ML";
 ML_file "Tools/generated_files.ML"
-
--- a/src/Pure/System/bash.scala	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/System/bash.scala	Fri Mar 05 08:22:34 2021 +0100
@@ -108,7 +108,7 @@
     def terminate(): Unit = Isabelle_Thread.try_uninterruptible
     {
       kill("INT", count = 7) && kill("TERM", count = 3) && kill("KILL")
-      proc.destroy
+      proc.destroy()
       do_cleanup()
     }
 
@@ -173,7 +173,7 @@
       watchdog: Option[Watchdog] = None,
       strict: Boolean = true): Process_Result =
     {
-      stdin.close
+      stdin.close()
 
       val out_lines =
         Future.thread("bash_stdout") { File.read_lines(stdout, progress_stdout) }
@@ -195,7 +195,7 @@
         try { join }
         catch { case Exn.Interrupt() => terminate(); Exn.Interrupt.return_code }
 
-      watchdog_thread.foreach(_.cancel)
+      watchdog_thread.foreach(_.cancel())
 
       if (strict && rc == Exn.Interrupt.return_code) throw Exn.Interrupt()
 
--- a/src/Pure/System/getopts.scala	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/System/getopts.scala	Fri Mar 05 08:22:34 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/isabelle_charset.scala	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/System/isabelle_charset.scala	Fri Mar 05 08:22:34 2021 +0100
@@ -12,8 +12,6 @@
 import java.nio.charset.{Charset, CharsetDecoder, CharsetEncoder, CoderResult}
 import java.nio.charset.spi.CharsetProvider
 
-import scala.collection.JavaConverters
-
 
 object Isabelle_Charset
 {
@@ -47,6 +45,6 @@
   {
     // FIXME inactive
     // Iterator(Isabelle_Charset.charset)
-    JavaConverters.asJavaIterator(Iterator())
+    java.util.List.of[Charset]().listIterator()
   }
 }
--- a/src/Pure/System/isabelle_process.scala	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/System/isabelle_process.scala	Fri Mar 05 08:22:34 2021 +0100
@@ -37,7 +37,7 @@
           modes = modes, cwd = cwd, env = env)
       }
       catch { case exn @ ERROR(_) => channel.shutdown(); throw exn }
-    process.stdin.close
+    process.stdin.close()
 
     new Isabelle_Process(session, channel, process)
   }
@@ -77,5 +77,5 @@
     result
   }
 
-  def terminate: Unit = process.terminate
+  def terminate(): Unit = process.terminate()
 }
--- a/src/Pure/System/isabelle_system.scala	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/System/isabelle_system.scala	Fri Mar 05 08:22:34 2021 +0100
@@ -421,7 +421,7 @@
     proc.command(command_line:_*)  // fragile on Windows
     if (cwd != null) proc.directory(cwd)
     if (env != null) {
-      proc.environment.clear
+      proc.environment.clear()
       for ((x, y) <- env) proc.environment.put(x, y)
     }
     proc.redirectErrorStream(redirect)
@@ -430,15 +430,15 @@
 
   def process_output(proc: Process): (String, Int) =
   {
-    proc.getOutputStream.close
+    proc.getOutputStream.close()
 
     val output = File.read_stream(proc.getInputStream)
     val rc =
       try { proc.waitFor }
       finally {
-        proc.getInputStream.close
-        proc.getErrorStream.close
-        proc.destroy
+        proc.getInputStream.close()
+        proc.getErrorStream.close()
+        proc.destroy()
         Exn.Interrupt.dispose()
       }
     (output, rc)
--- a/src/Pure/System/isabelle_tool.scala	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/System/isabelle_tool.scala	Fri Mar 05 08:22:34 2021 +0100
@@ -29,11 +29,14 @@
     val tool_box = universe.runtimeMirror(class_loader).mkToolBox()
 
     try {
-      val symbol = tool_box.parse(source) match {
-        case tree: universe.ModuleDef => tool_box.define(tree)
-        case _ => err("Source does not describe a module (Scala object)")
-      }
-      tool_box.compile(universe.Ident(symbol))() match {
+      val tree = tool_box.parse(source)
+      val module =
+        try { tree.asInstanceOf[universe.ModuleDef] }
+        catch {
+          case _: java.lang.ClassCastException =>
+            err("Source does not describe a module (Scala object)")
+        }
+      tool_box.compile(universe.Ident(tool_box.define(module)))() match {
         case body: Body => body
         case _ => err("Ill-typed source: Isabelle_Tool.Body expected")
       }
@@ -157,7 +160,7 @@
 
   Start Isabelle TOOL with ARGS; pass "-?" for tool-specific help.
 
-Available tools:""" + tool_descriptions.mkString("\n  ", "\n  ", "\n")).usage
+Available tools:""" + tool_descriptions.mkString("\n  ", "\n  ", "\n")).usage()
         case tool_name :: tool_args =>
           find_external(tool_name) orElse find_internal(tool_name) match {
             case Some(tool) => tool(tool_args)
--- a/src/Pure/System/options.scala	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/System/options.scala	Fri Mar 05 08:22:34 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/System/posix_interrupt.scala	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/System/posix_interrupt.scala	Fri Mar 05 08:22:34 2021 +0100
@@ -23,7 +23,7 @@
   def exception[A](e: => A): A =
   {
     val thread = Thread.currentThread
-    handler { thread.interrupt } { e }
+    handler { thread.interrupt() } { e }
   }
 }
 
--- a/src/Pure/System/progress.scala	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/System/progress.scala	Fri Mar 05 08:22:34 2021 +0100
@@ -37,14 +37,14 @@
     Timing.timeit(message, enabled, echo)(e)
 
   @volatile protected var is_stopped = false
-  def stop: Unit = { is_stopped = true }
+  def stop(): Unit = { is_stopped = true }
   def stopped: Boolean =
   {
-    if (Thread.interrupted) is_stopped = true
+    if (Thread.interrupted()) is_stopped = true
     is_stopped
   }
 
-  def interrupt_handler[A](e: => A): A = POSIX_Interrupt.handler { stop } { e }
+  def interrupt_handler[A](e: => A): A = POSIX_Interrupt.handler { stop() } { e }
   def expose_interrupt(): Unit = if (stopped) throw Exn.Interrupt()
   override def toString: String = if (stopped) "Progress(stopped)" else "Progress"
 
--- a/src/Pure/System/scala.scala	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/System/scala.scala	Fri Mar 05 08:22:34 2021 +0100
@@ -114,7 +114,7 @@
             if (interpret) interp.interpret(source) == Results.Success
             else (new interp.ReadEvalPrint).compile(source)
           }
-        out.close
+        out.close()
 
         val Error = """(?s)^\S* error: (.*)$""".r
         val errors =
@@ -195,7 +195,7 @@
 
     private def cancel(id: String, future: Future[Unit]): Unit =
     {
-      future.cancel
+      future.cancel()
       result(id, Scala.Tag.INTERRUPT, "")
     }
 
--- a/src/Pure/System/system_channel.scala	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/System/system_channel.scala	Fri Mar 05 08:22:34 2021 +0100
@@ -25,7 +25,7 @@
 
   override def toString: String = address
 
-  def shutdown(): Unit = server.close
+  def shutdown(): Unit = server.close()
 
   def rendezvous(): (OutputStream, InputStream) =
   {
@@ -36,8 +36,8 @@
 
       if (Byte_Message.read_line(in_stream).map(_.text) == Some(password)) (out_stream, in_stream)
       else {
-        out_stream.close
-        in_stream.close
+        out_stream.close()
+        in_stream.close()
         error("Failed to connect system channel: bad password")
       }
     }
--- a/src/Pure/System/tty_loop.scala	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/System/tty_loop.scala	Fri Mar 05 08:22:34 2021 +0100
@@ -30,7 +30,7 @@
         if (result.nonEmpty) {
           System.out.print(result.toString)
           System.out.flush()
-          result.clear
+          result.clear()
         }
         else {
           reader.close()
@@ -64,5 +64,5 @@
 
   def join: Unit = { console_output.join; console_input.join }
 
-  def cancel: Unit = console_input.cancel
+  def cancel(): Unit = console_input.cancel()
 }
--- a/src/Pure/Thy/bibtex.scala	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/Thy/bibtex.scala	Fri Mar 05 08:22:34 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	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/Thy/export_theory.scala	Fri Mar 05 08:22:34 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	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/Thy/file_format.scala	Fri Mar 05 08:22:34 2021 +0100
@@ -39,15 +39,15 @@
       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)
+    def stop_session: Unit = agents.foreach(_.stop())
   }
 
   trait Agent
   {
     def prover_options(options: Options): Options = options
-    def stop: Unit = {}
+    def stop(): Unit = {}
   }
 
   object No_Agent extends Agent
--- a/src/Pure/Thy/latex.scala	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/Thy/latex.scala	Fri Mar 05 08:22:34 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	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/Thy/sessions.scala	Fri Mar 05 08:22:34 2021 +0100
@@ -11,7 +11,7 @@
 import java.nio.channels.FileChannel
 import java.nio.file.StandardOpenOption
 
-import scala.collection.{SortedSet, SortedMap}
+import scala.collection.immutable.{SortedSet, SortedMap}
 import scala.collection.mutable
 
 
@@ -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)
   }
@@ -1210,7 +1214,7 @@
   {
     def cache: XML.Cache = store.cache
 
-    def close: Unit = database_server.foreach(_.close)
+    def close(): Unit = database_server.foreach(_.close())
 
     def output_database[A](session: String)(f: SQL.Database => A): A =
       database_server match {
@@ -1346,7 +1350,7 @@
     def try_open_database(name: String, output: Boolean = false): Option[SQL.Database] =
     {
       def check(db: SQL.Database): Option[SQL.Database] =
-        if (output || session_info_exists(db)) Some(db) else { db.close; None }
+        if (output || session_info_exists(db)) Some(db) else { db.close(); None }
 
       if (database_server) check(open_database_server())
       else if (output) Some(SQLite.open_database(output_database(name)))
@@ -1376,7 +1380,7 @@
                   init_session_info(db, name)
                   relevant_db
                 }
-              } finally { db.close }
+              } finally { db.close() }
             case None => false
           }
         }
@@ -1416,16 +1420,16 @@
       db.transaction {
         db.create_table(Session_Info.table)
         db.using_statement(
-          Session_Info.table.delete(Session_Info.session_name.where_equal(name)))(_.execute)
+          Session_Info.table.delete(Session_Info.session_name.where_equal(name)))(_.execute())
 
         db.create_table(Export.Data.table)
         db.using_statement(
-          Export.Data.table.delete(Export.Data.session_name.where_equal(name)))(_.execute)
+          Export.Data.table.delete(Export.Data.session_name.where_equal(name)))(_.execute())
 
         db.create_table(Presentation.Data.table)
         db.using_statement(
           Presentation.Data.table.delete(
-            Presentation.Data.session_name.where_equal(name)))(_.execute)
+            Presentation.Data.session_name.where_equal(name)))(_.execute())
       }
     }
 
--- a/src/Pure/Thy/thy_header.scala	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/Thy/thy_header.scala	Fri Mar 05 08:22:34 2021 +0100
@@ -186,10 +186,10 @@
   private def read_tokens(reader: Reader[Char], strict: Boolean): (List[Token], List[Token]) =
   {
     val token = Token.Parsers.token(bootstrap_keywords)
-    def make_tokens(in: Reader[Char]): Stream[Token] =
+    def make_tokens(in: Reader[Char]): LazyList[Token] =
       token(in) match {
         case Token.Parsers.Success(tok, rest) => tok #:: make_tokens(rest)
-        case _ => Stream.empty
+        case _ => LazyList.empty
       }
 
     val all_tokens = make_tokens(reader)
@@ -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	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/Thy/thy_syntax.scala	Fri Mar 05 08:22:34 2021 +0100
@@ -27,7 +27,7 @@
       val visible = new mutable.ListBuffer[Command]
       val visible_overlay = new mutable.ListBuffer[Command]
       @tailrec
-      def check_ranges(ranges: List[Text.Range], commands: Stream[(Command, Text.Offset)]): Unit =
+      def check_ranges(ranges: List[Text.Range], commands: LazyList[(Command, Text.Offset)]): Unit =
       {
         (ranges, commands) match {
           case (range :: more_ranges, (command, offset) #:: more_commands) =>
@@ -55,7 +55,7 @@
 
       val commands =
         (if (overlays.is_empty) node.command_iterator(perspective.range)
-         else node.command_iterator()).toStream
+         else node.command_iterator()).to(LazyList)
       check_ranges(perspective.ranges, commands)
       (Command.Perspective(visible.toList), Command.Perspective(visible_overlay.toList))
     }
@@ -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	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/Tools/build.scala	Fri Mar 05 08:22:34 2021 +0100
@@ -8,7 +8,7 @@
 package isabelle
 
 
-import scala.collection.SortedSet
+import scala.collection.immutable.SortedSet
 import scala.annotation.tailrec
 
 
@@ -60,7 +60,7 @@
             case exn: java.lang.Error => ignore_error(Exn.message(exn))
             case _: XML.Error => ignore_error("")
           }
-          finally { db.close }
+          finally { db.close() }
       }
     }
 
@@ -99,16 +99,8 @@
 
       object Ordering extends scala.math.Ordering[String]
       {
-        def compare_timing(name1: String, name2: String): Int =
-        {
-          val t1 = session_timing(name1)
-          val t2 = session_timing(name2)
-          if (t1 == 0.0 || t2 == 0.0) 0
-          else t1 compare t2
-        }
-
         def compare(name1: String, name2: String): Int =
-          compare_timing(name2, name1) match {
+          session_timing(name2) compare session_timing(name1) match {
             case 0 =>
               sessions_structure(name2).timeout compare sessions_structure(name1).timeout match {
                 case 0 => name1 compare name2
@@ -132,16 +124,11 @@
     def is_empty: Boolean = graph.is_empty
 
     def - (name: String): Queue =
-      new Queue(graph.del_node(name),
-        order - name,  // FIXME scala-2.10.0 .. 2.12.4 TreeSet problem!?
-        command_timings)
+      new Queue(graph.del_node(name), order - name, command_timings)
 
     def dequeue(skip: String => Boolean): Option[(String, Sessions.Info)] =
     {
-      val it = order.iterator.dropWhile(name =>
-        skip(name)
-          || !graph.defined(name)  // FIXME scala-2.10.0 .. 2.12.4 TreeSet problem!?
-          || !graph.is_minimal(name))
+      val it = order.iterator.dropWhile(name => skip(name) || !graph.is_minimal(name))
       if (it.hasNext) { val name = it.next(); Some((name, graph.get_node(name))) }
       else None
     }
@@ -159,8 +146,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
@@ -303,7 +290,7 @@
     }
 
     def sleep(): Unit =
-      Isabelle_Thread.interrupt_handler(_ => progress.stop) { Time.seconds(0.5).sleep }
+      Isabelle_Thread.interrupt_handler(_ => progress.stop()) { Time.seconds(0.5).sleep }
 
     val numa_nodes = new NUMA.Nodes(numa_shuffling)
 
@@ -319,7 +306,7 @@
       if (pending.is_empty) results
       else {
         if (progress.stopped) {
-          for ((_, (_, job)) <- running) job.terminate
+          for ((_, (_, job)) <- running) job.terminate()
         }
 
         running.find({ case (_, (_, job)) => job.is_finished }) match {
@@ -661,7 +648,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/build_job.scala	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/Tools/build_job.scala	Fri Mar 05 08:22:34 2021 +0100
@@ -253,7 +253,7 @@
         private val promise: Promise[List[String]] = Future.promise
 
         def result: Exn.Result[List[String]] = promise.join_result
-        def cancel: Unit = promise.cancel
+        def cancel(): Unit = promise.cancel()
         def apply(errs: List[String]): Unit =
         {
           try { promise.fulfill(errs) }
@@ -286,7 +286,7 @@
 
       session.init_protocol_handler(new Session.Protocol_Handler
         {
-          override def exit(): Unit = Build_Session_Errors.cancel
+          override def exit(): Unit = Build_Session_Errors.cancel()
 
           private def build_session_finished(msg: Prover.Protocol_Output): Boolean =
           {
@@ -416,8 +416,8 @@
           cwd = info.dir.file, env = env)
 
       val build_errors =
-        Isabelle_Thread.interrupt_handler(_ => process.terminate) {
-          Exn.capture { process.await_startup } match {
+        Isabelle_Thread.interrupt_handler(_ => process.terminate()) {
+          Exn.capture { process.await_startup() } match {
             case Exn.Res(_) =>
               val resources_yxml = resources.init_session_yxml
               val args_yxml =
@@ -434,7 +434,7 @@
         }
 
       val process_result =
-        Isabelle_Thread.interrupt_handler(_ => process.terminate) { process.await_shutdown }
+        Isabelle_Thread.interrupt_handler(_ => process.terminate()) { process.await_shutdown() }
 
       session.stop()
 
@@ -502,13 +502,13 @@
       }
     }
 
-  def terminate: Unit = future_result.cancel
+  def terminate(): Unit = future_result.cancel()
   def is_finished: Boolean = future_result.is_finished
 
   private val timeout_request: Option[Event_Timer.Request] =
   {
     if (info.timeout > Time.zero)
-      Some(Event_Timer.request(Time.now() + info.timeout) { terminate })
+      Some(Event_Timer.request(Time.now() + info.timeout) { terminate() })
     else None
   }
 
@@ -519,7 +519,7 @@
     val was_timeout =
       timeout_request match {
         case None => false
-        case Some(request) => !request.cancel
+        case Some(request) => !request.cancel()
       }
 
     val result2 =
--- a/src/Pure/Tools/dump.scala	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/Tools/dump.scala	Fri Mar 05 08:22:34 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	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/Tools/scala_project.scala	Fri Mar 05 08:22:34 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	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/Tools/server.scala	Fri Mar 05 08:22:34 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 */
@@ -148,9 +149,9 @@
         }
       }
 
-    def start: Unit = thread
+    def start(): Unit = thread
     def join: Unit = thread.join
-    def stop: Unit = { socket.close; join }
+    def stop(): Unit = { socket.close(); join }
   }
 
 
@@ -166,7 +167,7 @@
   {
     override def toString: String = socket.toString
 
-    def close(): Unit = socket.close
+    def close(): Unit = socket.close()
 
     def set_timeout(t: Time): Unit = socket.setSoTimeout(t.ms.toInt)
 
@@ -249,11 +250,11 @@
       _tasks.change(_ - task)
 
     def cancel_task(id: UUID.T): Unit =
-      _tasks.change(tasks => { tasks.find(task => task.id == id).foreach(_.cancel); tasks })
+      _tasks.change(tasks => { tasks.find(task => task.id == id).foreach(_.cancel()); tasks })
 
     def close(): Unit =
     {
-      while(_tasks.change_result(tasks => { tasks.foreach(_.cancel); (tasks.nonEmpty, tasks) }))
+      while(_tasks.change_result(tasks => { tasks.foreach(_.cancel()); (tasks.nonEmpty, tasks) }))
       { _tasks.value.foreach(_.join) }
     }
   }
@@ -292,7 +293,7 @@
     val ident: JSON.Object.Entry = ("task" -> id.toString)
 
     val progress: Connection_Progress = context.progress(ident)
-    def cancel: Unit = progress.stop
+    def cancel(): Unit = progress.stop()
 
     private lazy val thread = Isabelle_Thread.fork(name = "server_task")
     {
@@ -303,7 +304,7 @@
           val err = json_error(exn)
           if (err.isEmpty) throw exn else context.reply(Reply.FAILED, err + ident)
       }
-      progress.stop
+      progress.stop()
       context.remove_task(task)
     }
     def start: Unit = thread
@@ -350,7 +351,7 @@
       connection
     }
 
-    def active(): Boolean =
+    def active: Boolean =
       try {
         using(connection())(connection =>
           {
@@ -410,7 +411,7 @@
           db.create_table(Data.table)
           list(db).filterNot(_.active).foreach(server_info =>
             db.using_statement(Data.table.delete(Data.name.where_equal(server_info.name)))(
-              _.execute))
+              _.execute()))
         }
         db.transaction {
           find(db, name) match {
@@ -421,7 +422,7 @@
               val server = new Server(port, log)
               val server_info = Info(name, server.port, server.password)
 
-              db.using_statement(Data.table.delete(Data.name.where_equal(name)))(_.execute)
+              db.using_statement(Data.table.delete(Data.name.where_equal(name)))(_.execute())
               db.using_statement(Data.table.insert())(stmt =>
               {
                 stmt.string(1) = server_info.name
@@ -430,7 +431,7 @@
                 stmt.execute()
               })
 
-              server.start
+              server.start()
               (server_info, Some(server))
           }
         }
@@ -533,7 +534,7 @@
 
   def shutdown(): Unit =
   {
-    server.socket.close
+    server.socket.close()
 
     val sessions = _sessions.change_result(sessions => (sessions, Map.empty))
     for ((_, session) <- sessions) {
--- a/src/Pure/Tools/spell_checker.scala	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/Tools/spell_checker.scala	Fri Mar 05 08:22:34 2021 +0100
@@ -88,7 +88,7 @@
     }
   }
 
-  def dictionaries(): List[Dictionary] =
+  def dictionaries: List[Dictionary] =
     for {
       path <- Path.split(Isabelle_System.getenv("JORTHO_DICTIONARIES"))
       if path.is_file
--- a/src/Pure/library.scala	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/library.scala	Fri Mar 05 08:22:34 2021 +0100
@@ -96,9 +96,11 @@
 
   /* lines */
 
-  def terminate_lines(lines: IterableOnce[String]): String = lines.mkString("", "\n", "\n")
+  def terminate_lines(lines: IterableOnce[String]): String =
+    lines.iterator.mkString("", "\n", "\n")
 
-  def cat_lines(lines: IterableOnce[String]): String = lines.mkString("\n")
+  def cat_lines(lines: IterableOnce[String]): String =
+    lines.iterator.mkString("\n")
 
   def split_lines(str: String): List[String] = space_explode('\n', str)
 
@@ -126,7 +128,9 @@
 
   /* strings */
 
-  def cat_strings0(strs: IterableOnce[String]): String = strs.mkString("\u0000")
+  def cat_strings0(strs: IterableOnce[String]): String =
+    strs.iterator.mkString("\u0000")
+
   def split_strings0(str: String): List[String] = space_explode('\u0000', str)
 
   def make_string(f: StringBuilder => Unit): String =
--- a/src/Tools/Graphview/graph_panel.scala	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Tools/Graphview/graph_panel.scala	Fri Mar 05 08:22:34 2021 +0100
@@ -341,8 +341,8 @@
     tooltip = "Use editor font and colors for painting"
   }
 
-  private val colorations = new Button { action = Action("Colorations") { color_dialog.open } }
-  private val filters = new Button { action = Action("Filters") { mutator_dialog.open } }
+  private val colorations = new Button { action = Action("Colorations") { color_dialog.open() } }
+  private val filters = new Button { action = Action("Filters") { mutator_dialog.open() } }
 
   private val controls =
     Wrap_Panel(
--- a/src/Tools/Graphview/layout.scala	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Tools/Graphview/layout.scala	Fri Mar 05 08:22:34 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	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Tools/Graphview/metrics.scala	Fri Mar 05 08:22:34 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	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Tools/Graphview/model.scala	Fri Mar 05 08:22:34 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	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Tools/Graphview/mutator.scala	Fri Mar 05 08:22:34 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/mutator_dialog.scala	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Tools/Graphview/mutator_dialog.scala	Fri Mar 05 08:22:34 2021 +0100
@@ -46,7 +46,7 @@
   override def open(): Unit =
   {
     if (!visible) panels = get_panels(container())
-    super.open
+    super.open()
   }
 
   minimumSize = new Dimension(700, 200)
@@ -94,8 +94,8 @@
 
   def paint_panels(): Unit =
   {
-    Focus_Traveral_Policy.clear
-    filter_panel.contents.clear
+    Focus_Traveral_Policy.clear()
+    filter_panel.contents.clear()
     panels.map(x => {
         filter_panel.contents += x
         Focus_Traveral_Policy.addAll(x.focusList)
@@ -106,8 +106,8 @@
     Focus_Traveral_Policy.add(add_button.peer)
     Focus_Traveral_Policy.add(apply_button.peer)
     Focus_Traveral_Policy.add(cancel_button.peer)
-    filter_panel.revalidate
-    filter_panel.repaint
+    filter_panel.revalidate()
+    filter_panel.repaint()
   }
 
   val filter_panel: BoxPanel = new BoxPanel(Orientation.Vertical) {}
@@ -130,7 +130,7 @@
   }
 
   private val cancel_button = new Button {
-    action = Action("Close") { close }
+    action = Action("Close") { close() }
   }
   defaultButton = cancel_button
 
--- a/src/Tools/Graphview/shapes.scala	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Tools/Graphview/shapes.scala	Fri Mar 05 08:22:34 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/language_server.scala	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Tools/VSCode/src/language_server.scala	Fri Mar 05 08:22:34 2021 +0100
@@ -136,7 +136,7 @@
       val (invoke_input, invoke_load) =
         resources.resolve_dependencies(session, editor, file_watcher)
       if (invoke_input) delay_input.invoke()
-      if (invoke_load) delay_load.invoke
+      if (invoke_load) delay_load.invoke()
     }
 
   private val file_watcher =
@@ -307,7 +307,7 @@
 
       try {
         Isabelle_Process(session, options, base_info.sessions_structure, Sessions.store(options),
-          modes = modes, logic = base_info.session).await_startup
+          modes = modes, logic = base_info.session).await_startup()
         reply_ok("Welcome to Isabelle/" + base_info.session + " (" + Distribution.version + ")")
       }
       catch { case ERROR(msg) => reply_error(msg) }
--- a/src/Tools/VSCode/src/preview_panel.scala	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Tools/VSCode/src/preview_panel.scala	Fri Mar 05 08:22:34 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	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Tools/VSCode/src/vscode_rendering.scala	Fri Mar 05 08:22:34 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	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Fri Mar 05 08:22:34 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-base/jedit_lib.scala	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Tools/jEdit/src-base/jedit_lib.scala	Fri Mar 05 08:22:34 2021 +0100
@@ -19,7 +19,7 @@
     val view = if (alt_view != null) alt_view else jEdit.getActiveView()
     if (view != null) {
       val text_area = view.getTextArea
-      if (text_area != null) text_area.requestFocus
+      if (text_area != null) text_area.requestFocus()
     }
   }
 }
\ No newline at end of file
--- a/src/Tools/jEdit/src/active.scala	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Tools/jEdit/src/active.scala	Fri Mar 05 08:22:34 2021 +0100
@@ -95,7 +95,7 @@
                   Isabelle.insert_line_padding(text_area, text)
                 else text_area.setSelectedText(text)
             }
-            text_area.requestFocus
+            text_area.requestFocus()
           }
           true
 
--- a/src/Tools/jEdit/src/completion_popup.scala	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Tools/jEdit/src/completion_popup.scala	Fri Mar 05 08:22:34 2021 +0100
@@ -281,7 +281,7 @@
               {
                 if (view.getKeyEventInterceptor == inner_key_listener)
                   view.setKeyEventInterceptor(null)
-                if (focus) text_area.requestFocus
+                if (focus) text_area.requestFocus()
                 JEdit_Lib.invalidate_range(text_area, range)
               }
             }
@@ -501,7 +501,7 @@
                   override def propagate(evt: KeyEvent): Unit =
                     if (!evt.isConsumed) text_field.processKeyEvent(evt)
                   override def shutdown(focus: Boolean): Unit =
-                    if (focus) text_field.requestFocus
+                    if (focus) text_field.requestFocus()
                 }
               dismissed()
               completion_popup = Some(completion)
@@ -703,7 +703,7 @@
   private def show_popup(focus: Boolean): Unit =
   {
     popup.show
-    if (focus) list_view.requestFocus
+    if (focus) list_view.requestFocus()
   }
 
   private def hide_popup(): Unit =
--- a/src/Tools/jEdit/src/debugger_dockable.scala	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Tools/jEdit/src/debugger_dockable.scala	Fri Mar 05 08:22:34 2021 +0100
@@ -298,7 +298,7 @@
 
   /* focus */
 
-  override def focusOnDefaultComponent(): Unit = eval_button.requestFocus
+  override def focusOnDefaultComponent(): Unit = eval_button.requestFocus()
 
   addFocusListener(new FocusAdapter {
     override def focusGained(e: FocusEvent): Unit = update_focus()
--- a/src/Tools/jEdit/src/document_model.scala	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Fri Mar 05 08:22:34 2021 +0100
@@ -592,7 +592,7 @@
         val edits = get_edits
         val (reparse, perspective) = node_perspective(doc_blobs, hidden)
         if (reparse || edits.nonEmpty || last_perspective != perspective) {
-          pending.clear
+          pending.clear()
           last_perspective = perspective
           node_edits(node_header(), edits, perspective)
         }
--- a/src/Tools/jEdit/src/isabelle.scala	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Tools/jEdit/src/isabelle.scala	Fri Mar 05 08:22:34 2021 +0100
@@ -616,5 +616,5 @@
   /* java monitor */
 
   def java_monitor(view: View): Unit =
-    Java_Monitor.java_monitor_external(view, look_and_feel = GUI.current_laf())
+    Java_Monitor.java_monitor_external(view, look_and_feel = GUI.current_laf)
 }
--- a/src/Tools/jEdit/src/isabelle_sidekick.scala	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Tools/jEdit/src/isabelle_sidekick.scala	Fri Mar 05 08:22:34 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
       }
     }
 
@@ -179,7 +180,7 @@
   {
     val opt_snapshot =
       Document_Model.get(buffer) match {
-        case Some(model) if model.is_theory => Some(model.snapshot)
+        case Some(model) if model.is_theory => Some(model.snapshot())
         case _ => None
       }
     opt_snapshot match {
--- a/src/Tools/jEdit/src/jedit_editor.scala	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Fri Mar 05 08:22:34 2021 +0100
@@ -66,7 +66,7 @@
   {
     GUI_Thread.require {}
     Document_Model.get(name) match {
-      case Some(model) => model.snapshot
+      case Some(model) => model.snapshot()
       case None => session.snapshot(name)
     }
   }
--- a/src/Tools/jEdit/src/jedit_lib.scala	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Fri Mar 05 08:22:34 2021 +0100
@@ -50,7 +50,7 @@
 
     dummy_window.setContentPane(outer)
     dummy_window.pack
-    dummy_window.revalidate
+    dummy_window.revalidate()
 
     val geometry =
       Window_Geometry(
--- a/src/Tools/jEdit/src/jedit_sessions.scala	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Tools/jEdit/src/jedit_sessions.scala	Fri Mar 05 08:22:34 2021 +0100
@@ -18,10 +18,10 @@
 {
   /* session options */
 
-  def session_dirs(): List[Path] =
+  def session_dirs: List[Path] =
     Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS")).filterNot(p => p.implode == "-")
 
-  def session_no_build(): Boolean =
+  def session_no_build: Boolean =
     Isabelle_System.getenv("JEDIT_NO_BUILD") == "true"
 
   def session_options(options: Options): Options =
@@ -41,7 +41,7 @@
     options2
   }
 
-  def sessions_structure(options: Options, dirs: List[Path] = session_dirs()): Sessions.Structure =
+  def sessions_structure(options: Options, dirs: List[Path] = session_dirs): Sessions.Structure =
     Sessions.load_structure(session_options(options), dirs = dirs)
 
 
@@ -119,7 +119,7 @@
 
   def session_base_info(options: Options): Sessions.Base_Info =
     Sessions.base_info(options,
-      dirs = JEdit_Sessions.session_dirs(),
+      dirs = JEdit_Sessions.session_dirs,
       include_sessions = logic_include_sessions,
       session = logic_name(options),
       session_ancestor = logic_ancestor,
@@ -130,7 +130,7 @@
   {
     Build.build(session_options(options),
       selection = Sessions.Selection.session(PIDE.resources.session_name),
-      progress = progress, build_heap = true, no_build = no_build, dirs = session_dirs(),
+      progress = progress, build_heap = true, no_build = no_build, dirs = session_dirs,
       infos = PIDE.resources.session_base_info.infos).rc
   }
 
--- a/src/Tools/jEdit/src/jedit_spell_checker.scala	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Tools/jEdit/src/jedit_spell_checker.scala	Fri Mar 05 08:22:34 2021 +0100
@@ -87,7 +87,7 @@
     val option_name = "spell_checker_dictionary"
     val opt = PIDE.options.value.check_name(option_name)
 
-    val entries = Spell_Checker.dictionaries()
+    val entries = Spell_Checker.dictionaries
     val component = new ComboBox(entries) with Option_Component {
       name = option_name
       val title = opt.title()
--- a/src/Tools/jEdit/src/plugin.scala	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Tools/jEdit/src/plugin.scala	Fri Mar 05 08:22:34 2021 +0100
@@ -29,7 +29,7 @@
   def maybe_snapshot(view: View = null): Option[Document.Snapshot] = GUI_Thread.now
   {
     val buffer = JEdit_Lib.jedit_view(view).getBuffer
-    Document_Model.get(buffer).map(_.snapshot)
+    Document_Model.get(buffer).map(_.snapshot())
   }
 
   def maybe_rendering(view: View = null): Option[JEdit_Rendering] = GUI_Thread.now
@@ -393,7 +393,7 @@
 
         case msg: PropertiesChanged =>
           for {
-            view <- JEdit_Lib.jedit_views
+            view <- JEdit_Lib.jedit_views()
             edit_pane <- JEdit_Lib.jedit_edit_panes(view)
           } {
             val buffer = edit_pane.getBuffer
@@ -458,13 +458,13 @@
       completion_history.load()
       spell_checker.update(options.value)
 
-      JEdit_Lib.jedit_views.foreach(init_title)
+      JEdit_Lib.jedit_views().foreach(init_title)
 
       isabelle.jedit_base.Syntax_Style.set_style_extender(Syntax_Style.Extender)
       init_mode_provider()
-      JEdit_Lib.jedit_text_areas.foreach(Completion_Popup.Text_Area.init)
+      JEdit_Lib.jedit_text_areas().foreach(Completion_Popup.Text_Area.init)
 
-      http_server.start
+      http_server.start()
 
       startup_failure = None
     }
@@ -483,11 +483,11 @@
 
   override def stop(): Unit =
   {
-    http_server.stop
+    http_server.stop()
 
     isabelle.jedit_base.Syntax_Style.dummy_style_extender()
     exit_mode_provider()
-    JEdit_Lib.jedit_text_areas.foreach(Completion_Popup.Text_Area.exit)
+    JEdit_Lib.jedit_text_areas().foreach(Completion_Popup.Text_Area.exit)
 
     if (startup_failure.isEmpty) {
       options.value.save_prefs()
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Fri Mar 05 08:22:34 2021 +0100
@@ -95,7 +95,7 @@
       val results = current_base_results
       val formatted_body = Pretty.formatted(current_body, margin = margin, metric = metric)
 
-      future_refresh.foreach(_.cancel)
+      future_refresh.foreach(_.cancel())
       future_refresh =
         Some(Future.fork {
           val (text, rendering) =
--- a/src/Tools/jEdit/src/pretty_tooltip.scala	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Fri Mar 05 08:22:34 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
@@ -280,12 +280,12 @@
   private def show_popup: Unit =
   {
     popup.show
-    pretty_text_area.requestFocus
+    pretty_text_area.requestFocus()
     pretty_text_area.update(rendering.snapshot, results, info.info)
   }
 
   private def hide_popup: Unit = popup.hide
 
-  private def request_focus: Unit = pretty_text_area.requestFocus
+  private def request_focus: Unit = pretty_text_area.requestFocus()
 }
 
--- a/src/Tools/jEdit/src/process_indicator.scala	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Tools/jEdit/src/process_indicator.scala	Fri Mar 05 08:22:34 2021 +0100
@@ -34,7 +34,7 @@
         {
           current_frame = (current_frame + 1) % active_icons.length
           setImage(active_icons(current_frame))
-          label.repaint
+          label.repaint()
         }
       })
     timer.setRepeats(true)
@@ -44,7 +44,7 @@
       if (rate == 0) {
         setImage(passive_icon)
         timer.stop
-        label.repaint
+        label.repaint()
       }
       else {
         val delay = 1000 / rate
--- a/src/Tools/jEdit/src/query_dockable.scala	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Tools/jEdit/src/query_dockable.scala	Fri Mar 05 08:22:34 2021 +0100
@@ -258,7 +258,7 @@
 
     def select: Unit =
     {
-      control_panel.contents.clear
+      control_panel.contents.clear()
       control_panel.contents += query_label
       update_items().foreach(item => control_panel.contents += item.checkbox)
       control_panel.contents ++=
@@ -291,13 +291,13 @@
 
   private def select_operation(): Unit =
   {
-    for (op <- get_operation()) { op.select; op.query.requestFocus }
-    operations_pane.revalidate
+    for (op <- get_operation()) { op.select; op.query.requestFocus() }
+    operations_pane.revalidate()
   }
 
   override def focusOnDefaultComponent(): Unit =
   {
-    for (op <- get_operation()) op.query.requestFocus
+    for (op <- get_operation()) op.query.requestFocus()
   }
 
   select_operation()
--- a/src/Tools/jEdit/src/rich_text_area.scala	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Fri Mar 05 08:22:34 2021 +0100
@@ -221,7 +221,7 @@
                 case _: ArrayIndexOutOfBoundsException =>
                 case _: IllegalArgumentException =>
               }
-              text_area.requestFocus
+              text_area.requestFocus()
             }
             link.follow(view)
           case None =>
--- a/src/Tools/jEdit/src/scala_console.scala	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Tools/jEdit/src/scala_console.scala	Fri Mar 05 08:22:34 2021 +0100
@@ -30,7 +30,7 @@
 
     override def flush(): Unit =
     {
-      val s = buf.synchronized { val s = buf.toString; buf.clear; s }
+      val s = buf.synchronized { val s = buf.toString; buf.clear(); s }
       val str = UTF8.decode_permissive(s)
       GUI_Thread.later {
         if (global_out == null) System.out.print(str)
@@ -97,7 +97,7 @@
   private class Interpreter
   {
     private val running = Synchronized[Option[Thread]](None)
-    def interrupt: Unit = running.change(opt => { opt.foreach(_.interrupt); opt })
+    def interrupt(): Unit = running.change(opt => { opt.foreach(_.interrupt()); opt })
 
     private val interp =
       Scala.Compiler.context(error = report_error, jar_dirs = JEdit_Lib.directories).
@@ -146,8 +146,8 @@
   {
     interpreters.get(console) match {
       case Some(interp) =>
-        interp.interrupt
-        interp.thread.shutdown
+        interp.interrupt()
+        interp.thread.shutdown()
         interpreters -= console
       case None =>
     }
@@ -177,5 +177,5 @@
   }
 
   override def stop(console: Console): Unit =
-    interpreters.get(console).foreach(_.interrupt)
+    interpreters.get(console).foreach(_.interrupt())
 }
--- a/src/Tools/jEdit/src/session_build.scala	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Tools/jEdit/src/session_build.scala	Fri Mar 05 08:22:34 2021 +0100
@@ -80,10 +80,10 @@
 
     private def set_actions(cs: Component*): Unit =
     {
-      action_panel.contents.clear
+      action_panel.contents.clear()
       action_panel.contents ++= cs
-      layout_panel.revalidate
-      layout_panel.repaint
+      layout_panel.revalidate()
+      layout_panel.repaint()
     }
 
 
@@ -94,7 +94,7 @@
     private def return_code(rc: Int): Unit =
       GUI_Thread.later {
         _return_code = Some(rc)
-        delay_exit.invoke
+        delay_exit.invoke()
       }
 
     private val delay_exit =
@@ -129,7 +129,7 @@
 
     private def stopping(): Unit =
     {
-      progress.stop
+      progress.stop()
       set_actions(new Label("Stopping ..."))
     }
 
--- a/src/Tools/jEdit/src/sledgehammer_dockable.scala	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala	Fri Mar 05 08:22:34 2021 +0100
@@ -145,7 +145,7 @@
 
   add(controls.peer, BorderLayout.NORTH)
 
-  override def focusOnDefaultComponent(): Unit = provers.requestFocus
+  override def focusOnDefaultComponent(): Unit = provers.requestFocus()
 
 
   /* main */
--- a/src/Tools/jEdit/src/symbols_dockable.scala	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Tools/jEdit/src/symbols_dockable.scala	Fri Mar 05 08:22:34 2021 +0100
@@ -43,7 +43,7 @@
           Completion.split_template(Isabelle_Encoding.perhaps_decode(text_area.getBuffer, txt))
         text_area.setSelectedText(s1 + s2)
         text_area.moveCaretPosition(text_area.getCaretPosition - s2.length)
-        text_area.requestFocus
+        text_area.requestFocus()
       }
     tooltip = GUI.tooltip_lines(cat_lines(txt :: abbrs.map(a => "abbrev: " + a)))
   }
@@ -67,12 +67,12 @@
                 forall(s => s.length == 1 && s(0) != Completion.caret_indicator)
             } yield (txt, abbr)): _*).iterator_list.toList
 
-        contents.clear
+        contents.clear()
         for ((txt, abbrs) <- entries.sortBy(_._1))
           contents += new Abbrev_Component(txt, abbrs.filterNot(_ == "").sorted)
 
-        revalidate
-        repaint
+        revalidate()
+        repaint()
       }
     }
 
@@ -101,7 +101,7 @@
           Syntax_Style.edit_control_style(text_area, symbol)
         else
           text_area.setSelectedText(Isabelle_Encoding.perhaps_decode(text_area.getBuffer, symbol))
-        text_area.requestFocus
+        text_area.requestFocus()
       }
     tooltip =
       GUI.tooltip_lines(
@@ -113,7 +113,7 @@
     action = Action("Reset") {
       val text_area = view.getTextArea
       Syntax_Style.edit_control_style(text_area, "")
-      text_area.requestFocus
+      text_area.requestFocus()
     }
     tooltip = "Reset control symbols within text"
   }
@@ -135,14 +135,14 @@
         val results =
           for ((sym, s) <- search_space; if search_words.forall(s.contains(_))) yield sym
 
-        results_panel.contents.clear
+        results_panel.contents.clear()
         for (sym <- results.take(search_limit))
           results_panel.contents += new Symbol_Component(sym, false)
         if (results.length > search_limit)
           results_panel.contents +=
             new Label("...") { tooltip = "(" + (results.length - search_limit) + " more)" }
-        revalidate
-        repaint
+        revalidate()
+        repaint()
       }
       search_field.reactions += { case ValueChanged(_) => search_delay.invoke() }
   }
@@ -170,7 +170,7 @@
     listenTo(selection)
     reactions += {
       case SelectionChanged(_) if selection.page == search_page =>
-        search_panel.search_field.requestFocus
+        search_panel.search_field.requestFocus()
     }
 
     for (page <- pages)
--- a/src/Tools/jEdit/src/text_overview.scala	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Tools/jEdit/src/text_overview.scala	Fri Mar 05 08:22:34 2021 +0100
@@ -116,7 +116,7 @@
   private def is_running(): Boolean = !future_refresh.value.is_finished
 
   def invoke(): Unit = delay_refresh.invoke()
-  def revoke(): Unit = { delay_refresh.revoke(); future_refresh.change(x => { x.cancel; x }) }
+  def revoke(): Unit = { delay_refresh.revoke(); future_refresh.change(x => { x.cancel(); x }) }
 
   private val delay_refresh =
     Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) {
--- a/src/Tools/jEdit/src/text_structure.scala	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Tools/jEdit/src/text_structure.scala	Fri Mar 05 08:22:34 2021 +0100
@@ -93,7 +93,7 @@
                   (for {
                     text_area <- JEdit_Lib.jedit_text_areas(buffer)
                     doc_view <- Document_View.get(text_area)
-                  } yield doc_view.get_rendering).nextOption()
+                  } yield doc_view.get_rendering()).nextOption()
                 }
               else None
             val limit = PIDE.options.value.int("jedit_indent_script_limit")
@@ -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	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Tools/jEdit/src/theories_dockable.scala	Fri Mar 05 08:22:34 2021 +0100
@@ -25,7 +25,7 @@
 {
   /* status */
 
-  private val status = new ListView(Nil: List[Document.Node.Name]) {
+  private val status = new ListView(List.empty[Document.Node.Name]) {
     background =
     {
       // enforce default value
@@ -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	Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Tools/jEdit/src/timing_dockable.scala	Fri Mar 05 08:22:34 2021 +0100
@@ -104,7 +104,7 @@
 
   /* timing view */
 
-  private val timing_view = new ListView(Nil: List[Entry]) {
+  private val timing_view = new ListView(List.empty[Entry]) {
     listenTo(mouse.clicks)
     reactions += {
       case MouseClicked(_, point, _, clicks, _) if clicks == 2 =>
@@ -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()