# HG changeset patch
# User wenzelm
# Date 1493304885 -7200
# Node ID ffd8283b7be046c897f3cc28aea30ad4f35c7ec3
# Parent  6593057089599af92bbb5e6474b683e4736ebe11
support for database connection;

diff -r 659305708959 -r ffd8283b7be0 etc/options
--- a/etc/options	Thu Apr 27 15:56:55 2017 +0200
+++ b/etc/options	Thu Apr 27 16:54:45 2017 +0200
@@ -232,3 +232,15 @@
 
 option ssh_alive_interval : real = 30
   -- "time interval to keep SSH server connection alive (seconds)"
+
+
+section "Build Log Database"
+
+option build_log_database_user : string = ""
+option build_log_database_password : string = ""
+option build_log_database_name : string = ""
+option build_log_database_host : string = ""
+option build_log_database_port : int = 0
+option build_log_ssh_host : string = ""
+option build_log_ssh_user : string = ""
+option build_log_ssh_port : int = 0
diff -r 659305708959 -r ffd8283b7be0 src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Thu Apr 27 15:56:55 2017 +0200
+++ b/src/Pure/Admin/build_log.scala	Thu Apr 27 16:54:45 2017 +0200
@@ -573,4 +573,30 @@
       ml_statistics = if (ml_statistics) log_file.filter_props(ML_STATISTICS_MARKER) else Nil,
       task_statistics = if (task_statistics) log_file.filter_props("\ftask_statistics = ") else Nil)
   }
+
+
+
+  /** persistent store **/
+
+  def store(options: Options): Store = new Store(options)
+
+  class Store private[Build_Log](options: Options) extends Properties.Store
+  {
+    def open_database(
+      user: String = options.string("build_log_database_user"),
+      password: String = options.string("build_log_database_password"),
+      database: String = options.string("build_log_database_name"),
+      host: String = options.string("build_log_database_host"),
+      port: Int = options.int("build_log_database_port"),
+      ssh_host: String = options.string("build_log_ssh_host"),
+      ssh_user: String = options.string("build_log_ssh_user"),
+      ssh_port: Int = options.int("build_log_ssh_port")): PostgreSQL.Database =
+    {
+      PostgreSQL.open_database(
+        user = user, password = password, database = database, host = host, port = port,
+        ssh =
+          if (ssh_host == "") None
+          else Some(SSH.init_context(options).open_session(ssh_host, ssh_user, port)))
+    }
+  }
 }