support for database connection;
authorwenzelm
Thu Apr 27 16:54:45 2017 +0200 (2017-04-27)
changeset 65595ffd8283b7be0
parent 65594 659305708959
child 65596 7fffa01b2d2b
support for database connection;
etc/options
src/Pure/Admin/build_log.scala
     1.1 --- a/etc/options	Thu Apr 27 15:56:55 2017 +0200
     1.2 +++ b/etc/options	Thu Apr 27 16:54:45 2017 +0200
     1.3 @@ -232,3 +232,15 @@
     1.4  
     1.5  option ssh_alive_interval : real = 30
     1.6    -- "time interval to keep SSH server connection alive (seconds)"
     1.7 +
     1.8 +
     1.9 +section "Build Log Database"
    1.10 +
    1.11 +option build_log_database_user : string = ""
    1.12 +option build_log_database_password : string = ""
    1.13 +option build_log_database_name : string = ""
    1.14 +option build_log_database_host : string = ""
    1.15 +option build_log_database_port : int = 0
    1.16 +option build_log_ssh_host : string = ""
    1.17 +option build_log_ssh_user : string = ""
    1.18 +option build_log_ssh_port : int = 0
     2.1 --- a/src/Pure/Admin/build_log.scala	Thu Apr 27 15:56:55 2017 +0200
     2.2 +++ b/src/Pure/Admin/build_log.scala	Thu Apr 27 16:54:45 2017 +0200
     2.3 @@ -573,4 +573,30 @@
     2.4        ml_statistics = if (ml_statistics) log_file.filter_props(ML_STATISTICS_MARKER) else Nil,
     2.5        task_statistics = if (task_statistics) log_file.filter_props("\ftask_statistics = ") else Nil)
     2.6    }
     2.7 +
     2.8 +
     2.9 +
    2.10 +  /** persistent store **/
    2.11 +
    2.12 +  def store(options: Options): Store = new Store(options)
    2.13 +
    2.14 +  class Store private[Build_Log](options: Options) extends Properties.Store
    2.15 +  {
    2.16 +    def open_database(
    2.17 +      user: String = options.string("build_log_database_user"),
    2.18 +      password: String = options.string("build_log_database_password"),
    2.19 +      database: String = options.string("build_log_database_name"),
    2.20 +      host: String = options.string("build_log_database_host"),
    2.21 +      port: Int = options.int("build_log_database_port"),
    2.22 +      ssh_host: String = options.string("build_log_ssh_host"),
    2.23 +      ssh_user: String = options.string("build_log_ssh_user"),
    2.24 +      ssh_port: Int = options.int("build_log_ssh_port")): PostgreSQL.Database =
    2.25 +    {
    2.26 +      PostgreSQL.open_database(
    2.27 +        user = user, password = password, database = database, host = host, port = port,
    2.28 +        ssh =
    2.29 +          if (ssh_host == "") None
    2.30 +          else Some(SSH.init_context(options).open_session(ssh_host, ssh_user, port)))
    2.31 +    }
    2.32 +  }
    2.33  }