# HG changeset patch
# User wenzelm
# Date 1708600763 -3600
# Node ID fabe9f89911f69d5142fbe86cdd8118726cf53b8
# Parent  3abfc5ebabada6b5e56f29744c9835c0d2d98f7d
tuned;

diff -r 3abfc5ebabad -r fabe9f89911f src/Pure/ML/ml_heap.scala
--- a/src/Pure/ML/ml_heap.scala	Thu Feb 22 12:14:55 2024 +0100
+++ b/src/Pure/ML/ml_heap.scala	Thu Feb 22 12:19:23 2024 +0100
@@ -94,16 +94,13 @@
     }
 
     def read_digests(db: SQL.Database, names: Iterable[String]): Map[String, SHA1.Digest] = {
-      require(names.nonEmpty)
-
       db.execute_query_statement(
         Base.table.select(List(Base.name, Base.heap_digest),
           sql = Generic.name.where_member(names)),
         List.from[(String, String)],
         res => res.string(Base.name) -> res.string(Base.heap_digest)
-      ).flatMap({
-        case (_, "") => None
-        case (name, digest) => Some(name -> SHA1.fake_digest(digest))
+      ).collect({
+        case (name, digest) if digest.nonEmpty => name -> SHA1.fake_digest(digest)
       }).toMap
     }