diff -r b3ca4a6ed74b -r 87ebf5a50283 src/Pure/PIDE/document_status.scala
--- a/src/Pure/PIDE/document_status.scala	Fri Apr 01 11:51:42 2022 +0200
+++ b/src/Pure/PIDE/document_status.scala	Fri Apr 01 17:06:10 2022 +0200
@@ -7,12 +7,10 @@
 package isabelle
 
 
-object Document_Status
-{
+object Document_Status {
   /* command status */
 
-  object Command_Status
-  {
+  object Command_Status {
     val proper_elements: Markup.Elements =
       Markup.Elements(Markup.ACCEPTED, Markup.FORKED, Markup.JOINED, Markup.RUNNING,
         Markup.FINISHED, Markup.FAILED, Markup.CANCELED)
@@ -20,8 +18,7 @@
     val liberal_elements: Markup.Elements =
       proper_elements + Markup.WARNING + Markup.LEGACY + Markup.ERROR
 
-    def make(markup_iterator: Iterator[Markup]): Command_Status =
-    {
+    def make(markup_iterator: Iterator[Markup]): Command_Status = {
       var touched = false
       var accepted = false
       var warned = false
@@ -73,8 +70,8 @@
     private val canceled: Boolean,
     private val finalized: Boolean,
     forks: Int,
-    runs: Int)
-  {
+    runs: Int
+  ) {
     def + (that: Command_Status): Command_Status =
       Command_Status(
         touched = touched || that.touched,
@@ -99,13 +96,11 @@
 
   /* node status */
 
-  object Node_Status
-  {
+  object Node_Status {
     def make(
       state: Document.State,
       version: Document.Version,
-      name: Document.Node.Name): Node_Status =
-    {
+      name: Document.Node.Name): Node_Status = {
       val node = version.nodes(name)
 
       var unprocessed = 0
@@ -159,8 +154,8 @@
     terminated: Boolean,
     initialized: Boolean,
     finalized: Boolean,
-    consolidated: Boolean)
-  {
+    consolidated: Boolean
+  ) {
     def ok: Boolean = failed == 0
     def total: Int = unprocessed + running + warned + failed + finished
 
@@ -181,16 +176,15 @@
 
   /* overall timing */
 
-  object Overall_Timing
-  {
+  object Overall_Timing {
     val empty: Overall_Timing = Overall_Timing(0.0, Map.empty)
 
     def make(
       state: Document.State,
       version: Document.Version,
       commands: Iterable[Command],
-      threshold: Double = 0.0): Overall_Timing =
-    {
+      threshold: Double = 0.0
+    ): Overall_Timing = {
       var total = 0.0
       var command_timings = Map.empty[Command, Double]
       for {
@@ -211,8 +205,7 @@
     }
   }
 
-  sealed case class Overall_Timing(total: Double, command_timings: Map[Command, Double])
-  {
+  sealed case class Overall_Timing(total: Double, command_timings: Map[Command, Double]) {
     def command_timing(command: Command): Double =
       command_timings.getOrElse(command, 0.0)
   }
@@ -220,20 +213,18 @@
 
   /* nodes status */
 
-  object Overall_Node_Status extends Enumeration
-  {
+  object Overall_Node_Status extends Enumeration {
     val ok, failed, pending = Value
   }
 
-  object Nodes_Status
-  {
+  object Nodes_Status {
     val empty: Nodes_Status = new Nodes_Status(Map.empty, Document.Nodes.empty)
   }
 
   final class Nodes_Status private(
     private val rep: Map[Document.Node.Name, Node_Status],
-    nodes: Document.Nodes)
-  {
+    nodes: Document.Nodes
+  ) {
     def is_empty: Boolean = rep.isEmpty
     def apply(name: Document.Node.Name): Node_Status = rep(name)
     def get(name: Document.Node.Name): Option[Node_Status] = rep.get(name)
@@ -262,8 +253,8 @@
       state: Document.State,
       version: Document.Version,
       domain: Option[Set[Document.Node.Name]] = None,
-      trim: Boolean = false): (Boolean, Nodes_Status) =
-    {
+      trim: Boolean = false
+    ): (Boolean, Nodes_Status) = {
       val nodes1 = version.nodes
       val update_iterator =
         for {
@@ -285,8 +276,7 @@
         case _ => false
       }
 
-    override def toString: String =
-    {
+    override def toString: String = {
       var ok = 0
       var failed = 0
       var pending = 0