diff -r 128fb34338f7 -r 88e33d16f2de src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Fri Oct 17 15:30:38 2025 +0200 +++ b/src/Pure/PIDE/document.scala Fri Oct 17 15:56:10 2025 +0200 @@ -1110,6 +1110,11 @@ (state1.snippet(List(command1), doc_blobs), state1) } + def progress_theories: List[Document_ID.Exec] = + List.from( + for ((id, st) <- theories.iterator if st.document_status.timings.has_running) + yield id) + def theory_snapshot(id: Document_ID.Exec, document_blobs: Node.Name => Blobs): Option[Snapshot] = if (theories.isDefinedAt(id)) Some(end_theory(id, document_blobs)._1) else None