diff -r b3ca4a6ed74b -r 87ebf5a50283 src/Pure/General/graph.scala
--- a/src/Pure/General/graph.scala	Fri Apr 01 11:51:42 2022 +0200
+++ b/src/Pure/General/graph.scala	Fri Apr 01 17:06:10 2022 +0200
@@ -11,27 +11,25 @@
 import scala.annotation.tailrec
 
 
-object Graph
-{
-  class Duplicate[Key](val key: Key) extends Exception
-  {
+object Graph {
+  class Duplicate[Key](val key: Key) extends Exception {
     override def toString: String = "Graph.Duplicate(" + key.toString + ")"
   }
-  class Undefined[Key](val key: Key) extends Exception
-  {
+  class Undefined[Key](val key: Key) extends Exception {
     override def toString: String = "Graph.Undefined(" + key.toString + ")"
   }
-  class Cycles[Key](val cycles: List[List[Key]]) extends Exception
-  {
+  class Cycles[Key](val cycles: List[List[Key]]) extends Exception {
     override def toString: String = cycles.mkString("Graph.Cycles(", ",\n", ")")
   }
 
   def empty[Key, A](implicit ord: Ordering[Key]): Graph[Key, A] =
     new Graph[Key, A](SortedMap.empty(ord))
 
-  def make[Key, A](entries: List[((Key, A), List[Key])],
-    symmetric: Boolean = false)(implicit ord: Ordering[Key]): Graph[Key, A] =
-  {
+  def make[Key, A](
+    entries: List[((Key, A), List[Key])],
+    symmetric: Boolean = false)(
+    implicit ord: Ordering[Key]
+  ): Graph[Key, A] = {
     val graph1 =
       entries.foldLeft(empty[Key, A](ord)) {
         case (graph, ((x, info), _)) => graph.new_node(x, info)
@@ -68,8 +66,7 @@
 }
 
 
-final class Graph[Key, A] private(rep: SortedMap[Key, (A, (SortedSet[Key], SortedSet[Key]))])
-{
+final class Graph[Key, A] private(rep: SortedMap[Key, (A, (SortedSet[Key], SortedSet[Key]))]) {
   type Keys = SortedSet[Key]
   type Entry = (A, (Keys, Keys))
 
@@ -121,8 +118,8 @@
   def reachable_length(
     count: Key => Long,
     next: Key => Keys,
-    xs: List[Key]): Map[Key, Long] =
-  {
+    xs: List[Key]
+  ): Map[Key, Long] = {
     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 next(x).foldLeft(rs + (x -> length))(reach(length + count(x)))
@@ -138,10 +135,9 @@
     limit: Long,
     count: Key => Long,
     next: Key => Keys,
-    xs: List[Key]): Keys =
-  {
-    def reach(res: (Long, Keys), x: Key): (Long, Keys) =
-    {
+    xs: List[Key]
+  ): Keys = {
+    def reach(res: (Long, Keys), x: Key): (Long, Keys) = {
       val (n, rs) = res
       if (rs.contains(x)) res
       else next(x).foldLeft((n + count(x), rs + x))(reach)
@@ -160,10 +156,12 @@
   }
 
   /*reachable nodes with result in topological order (for acyclic graphs)*/
-  private def reachable(next: Key => Keys, xs: List[Key], rev: Boolean = false): (List[List[Key]], Keys) =
-  {
-    def reach(x: Key, reached: (List[Key], Keys)): (List[Key], Keys) =
-    {
+  private def reachable(
+    next: Key => Keys,
+    xs: List[Key],
+    rev: Boolean = false
+  ): (List[List[Key]], Keys) = {
+    def reach(x: Key, reached: (List[Key], Keys)): (List[Key], Keys) = {
       val (rs, r_set) = reached
       if (r_set(x)) reached
       else {
@@ -173,8 +171,7 @@
         (x :: rs1, r_set1)
       }
     }
-    def reachs(reached: (List[List[Key]], Keys), x: Key): (List[List[Key]], Keys) =
-    {
+    def reachs(reached: (List[List[Key]], Keys), x: Key): (List[List[Key]], Keys) = {
       val (rss, r_set) = reached
       val (rs, r_set1) = reach(x, (Nil, r_set))
       (rs :: rss, r_set1)
@@ -218,8 +215,7 @@
 
   /* node operations */
 
-  def new_node(x: Key, info: A): Graph[Key, A] =
-  {
+  def new_node(x: Key, info: A): Graph[Key, A] = {
     if (defined(x)) throw new Graph.Duplicate(x)
     else new Graph[Key, A](rep + (x -> (info, (empty_keys, empty_keys))))
   }
@@ -235,8 +231,7 @@
         map + (y -> (i, if (fst) (preds - x, succs) else (preds, succs - x)))
     }
 
-  def del_node(x: Key): Graph[Key, A] =
-  {
+  def del_node(x: Key): Graph[Key, A] = {
     val (preds, succs) = get_entry(x)._2
     new Graph[Key, A](
       succs.foldLeft(preds.foldLeft(rep - x)(del_adjacent(false, x)))(del_adjacent(true, x)))
@@ -271,8 +266,7 @@
 
   /* irreducible paths -- Hasse diagram */
 
-  private def irreducible_preds(x_set: Keys, path: List[Key], z: Key): List[Key] =
-  {
+  private def irreducible_preds(x_set: Keys, path: List[Key], z: Key): List[Key] = {
     def red(x: Key)(x1: Key) = is_edge(x, x1) && x1 != z
     @tailrec def irreds(xs0: List[Key], xs1: List[Key]): List[Key] =
       xs0 match {
@@ -286,8 +280,7 @@
     irreds(imm_preds(z).toList, Nil)
   }
 
-  def irreducible_paths(x: Key, y: Key): List[List[Key]] =
-  {
+  def irreducible_paths(x: Key, y: Key): List[List[Key]] = {
     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
@@ -298,8 +291,7 @@
 
   /* transitive closure and reduction */
 
-  private def transitive_step(z: Key): Graph[Key, A] =
-  {
+  private def transitive_step(z: Key): Graph[Key, A] = {
     val (preds, succs) = get_entry(z)._2
     var graph = this
     for (x <- preds; y <- succs) graph = graph.add_edge(x, y)
@@ -308,8 +300,7 @@
 
   def transitive_closure: Graph[Key, A] = keys_iterator.foldLeft(this)(_.transitive_step(_))
 
-  def transitive_reduction_acyclic: Graph[Key, A] =
-  {
+  def transitive_reduction_acyclic: Graph[Key, A] = {
     val trans = this.transitive_closure
     if (trans.iterator.exists({ case (x, (_, (_, succs))) => succs.contains(x) }))
       error("Cyclic graph")