diff -r 2c9c4ad4c816 -r 29dfe75c058b src/Pure/General/json_api.scala
--- a/src/Pure/General/json_api.scala	Tue Dec 21 21:07:26 2021 +0100
+++ b/src/Pure/General/json_api.scala	Tue Dec 21 21:27:26 2021 +0100
@@ -48,6 +48,25 @@
     def check_resource: Resource = check_data.resource
     def check_resources: List[Resource] = check_data.resources
 
+    def iterator: Iterator[Root] =
+    {
+      val init = Some(this)
+      new Iterator[Root] {
+        private var state: Option[Root] = init
+        def hasNext: Boolean = state.nonEmpty
+        def next(): Root =
+          state match {
+            case None => Iterator.empty.next()
+            case Some(res) =>
+              state = res.get_next.map(_.get_root())
+              res
+          }
+      }
+    }
+    def iterator_data: Iterator[Data] = iterator.map(_.check_data)
+    def iterator_resource: Iterator[Resource] = iterator.map(_.check_resource)
+    def iterator_resources: Iterator[Resource] = iterator.flatMap(_.check_resources)
+
     override def toString: String = "Root(" + (if (ok) "ok" else "errors") + ")"
   }