# HG changeset patch
# User wenzelm
# Date 1678025993 -3600
# Node ID 71e3e144dc08b83c000c397fddcabefe318eedf1
# Parent  6aae7486e94ae7fc3b4e9cbe6139657a28a8f48d
tuned;

diff -r 6aae7486e94a -r 71e3e144dc08 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Sun Mar 05 15:19:17 2023 +0100
+++ b/src/Pure/Thy/sessions.scala	Sun Mar 05 15:19:53 2023 +0100
@@ -1481,19 +1481,14 @@
 
     def clean_output(name: String): (Boolean, Boolean) = {
       val relevant_db =
-        database_server && {
-          try_open_database(name) match {
-            case Some(db) =>
-              using(db) { db =>
-                db.transaction {
-                  val relevant_db = session_info_defined(db, name)
-                  init_session_info(db, name)
-                  relevant_db
-                }
-              }
-            case None => false
-          }
-        }
+        database_server &&
+          using_option(try_open_database(name))(db =>
+            db.transaction {
+              val relevant_db = session_info_defined(db, name)
+              init_session_info(db, name)
+              relevant_db
+            }
+          ).getOrElse(false)
 
       val del =
         for {