tuned signature;
authorwenzelm
Thu, 15 Jun 2023 21:24:37 +0200
changeset 78165 d47b2a04fc04
parent 78164 5454bec8f5c6
child 78166 70041580b81e
tuned signature;
src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Thu Jun 15 17:29:29 2023 +0200
+++ b/src/Pure/Thy/sessions.scala	Thu Jun 15 21:24:37 2023 +0200
@@ -1496,6 +1496,7 @@
       input_dirs.map(_ + database(name)).find(_.is_file)
 
     def build_database_server: Boolean = options.bool("build_database_server")
+    def build_database_test: Boolean = options.bool("build_database_test")
 
     def open_database_server(): PostgreSQL.Database =
       PostgreSQL.open_database(
@@ -1515,7 +1516,7 @@
     val build_database: Path = Path.explode("$ISABELLE_HOME_USER/build.db")
 
     def open_build_database(): Option[SQL.Database] =
-      if (!options.bool("build_database_test")) None
+      if (!build_database_test) None
       else if (build_database_server) Some(open_database_server())
       else Some(SQLite.open_database(build_database, restrict = true))