diff -r 16135603d9c7 -r ff6c1a82270f src/Pure/Thy/sessions.scala --- a/src/Pure/Thy/sessions.scala Sat Aug 06 23:13:35 2022 +0200 +++ b/src/Pure/Thy/sessions.scala Sun Aug 07 12:22:43 2022 +0200 @@ -1207,30 +1207,6 @@ val table = SQL.Table("isabelle_session_info", build_log_columns ::: build_columns) } - class Database_Context private[Sessions]( - val store: Sessions.Store, - val database_server: Option[SQL.Database] - ) extends AutoCloseable { - def cache: Term.Cache = store.cache - - def close(): Unit = database_server.foreach(_.close()) - - def database_output[A](session: String)(f: SQL.Database => A): A = - database_server match { - case Some(db) => f(db) - case None => using(store.open_database(session, output = true))(f) - } - - override def toString: String = { - val s = - database_server match { - case Some(db) => db.toString - case None => "input_dirs = " + store.input_dirs.map(_.absolute).mkString(", ") - } - "Database_Context(" + s + ")" - } - } - def store(options: Options, cache: Term.Cache = Term.Cache.make()): Store = new Store(options, cache) @@ -1310,9 +1286,6 @@ port = options.int("build_database_ssh_port"))), ssh_close = true) - def open_database_context(server: Boolean = database_server): Database_Context = - new Database_Context(store, if (server) Some(open_database_server()) else None) - def try_open_database( name: String, output: Boolean = false,