# HG changeset patch # User wenzelm # Date 1687857472 -7200 # Node ID edf86c70953546b2737a9e1c3c31e56c7af2c7c5 # Parent fd0430a7b7a47da4980da82a1346abb6acb5eee9 more robust close() after failed initialization; diff -r fd0430a7b7a4 -r edf86c709535 src/Pure/Tools/build_process.scala --- a/src/Pure/Tools/build_process.scala Tue Jun 27 10:24:32 2023 +0200 +++ b/src/Pure/Tools/build_process.scala Tue Jun 27 11:17:52 2023 +0200 @@ -802,33 +802,40 @@ /* progress backed by database */ + private val _database_server: Option[SQL.Database] = + try { store.maybe_open_database_server() } + catch { case exn: Throwable => close(); throw exn } + private val _build_database: Option[SQL.Database] = - store.maybe_open_build_database(Build_Process.Data.database) + try { store.maybe_open_build_database(Build_Process.Data.database) } + catch { case exn: Throwable => close(); throw exn } private val _host_database: Option[SQL.Database] = - store.maybe_open_build_database(Host.Data.database) - - private val _database_server: Option[SQL.Database] = - store.maybe_open_database_server() + try { store.maybe_open_build_database(Host.Data.database) } + catch { case exn: Throwable => close(); throw exn } protected val (progress, worker_uuid) = synchronized { _build_database match { case None => (build_progress, UUID.random().toString) case Some(db) => - val progress_db = store.open_build_database(Progress.Data.database) - val progress = - new Database_Progress(progress_db, build_progress, - hostname = hostname, - context_uuid = build_uuid) - (progress, progress.agent_uuid) + try { + val progress_db = store.open_build_database(Progress.Data.database) + val progress = + new Database_Progress(progress_db, build_progress, + hostname = hostname, + context_uuid = build_uuid) + (progress, progress.agent_uuid) + } + catch { case exn: Throwable => close(); throw exn } } } protected val log: Logger = Logger.make_system_log(progress, build_options) def close(): Unit = synchronized { - _build_database.foreach(_.close()) - _host_database.foreach(_.close()) + Option(_database_server).flatten.foreach(_.close()) + Option(_build_database).flatten.foreach(_.close()) + Option(_host_database).flatten.foreach(_.close()) progress match { case db_progress: Database_Progress => db_progress.exit()