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,