src/Pure/Thy/sessions.scala

--- a/src/Pure/Thy/sessions.scala	Wed Jan 04 15:02:48 2023 +0100
+++ b/src/Pure/Thy/sessions.scala	Wed Jan 04 15:42:00 2023 +0100
@@ -109,6 +109,10 @@
   class Sources private(rep: Map[String, Source_File]) extends Iterable[Source_File] {
     override def toString: String = rep.values.toList.sortBy(_.name).mkString("Sources(", ", ", ")")
     override def iterator: Iterator[Source_File] = rep.valuesIterator
+
+    def get(name: String): Option[Source_File] = rep.get(name)
+    def apply(name: String): Source_File =
+      get(name).getOrElse(error("Missing session sources entry " + quote(name)))
   }