# HG changeset patch
# User wenzelm
# Date 1713260342 -7200
# Node ID c188068e41f19d2292542c100e0bc6a178d20fbb
# Parent  4b95a1d8b2c9b93e0ad4213060498a98240c747d
tuned;

diff -r 4b95a1d8b2c9 -r c188068e41f1 src/Pure/ML/ml_heap.scala
--- a/src/Pure/ML/ml_heap.scala	Tue Apr 16 11:20:30 2024 +0200
+++ b/src/Pure/ML/ml_heap.scala	Tue Apr 16 11:39:02 2024 +0200
@@ -298,14 +298,14 @@
         /* log_db */
 
         for (session <- sessions; path <- session.log_db) {
-          val file_uuid = Store.read_build_uuid(path, session.name)
-          private_data.read_log_db(db, session.name, old_uuid = file_uuid) match {
-            case Some(log_db) if file_uuid.isEmpty =>
+          val old_uuid = Store.read_build_uuid(path, session.name)
+          for (log_db <- private_data.read_log_db(db, session.name, old_uuid = old_uuid)) {
+            if (old_uuid.isEmpty) {
               progress.echo("Restoring " + session.log_db_name + " ...")
               Isabelle_System.make_directory(path.expand.dir)
               Bytes.write(path, log_db.content)
-            case Some(_) => error("Incoherent content for session database " + path.expand)
-            case None =>
+            }
+            else error("Incoherent content for session database " + path.expand)
           }
         }
       }