# HG changeset patch
# User wenzelm
# Date 1486584258 -3600
# Node ID b28bd9dfe1083abdd129e456805ae2b14e2c4249
# Parent  f8f76a501d2530511410f67d07acace5d059cffc
minimal support for PostgreSQL databases;

diff -r f8f76a501d25 -r b28bd9dfe108 Admin/components/components.sha1
--- a/Admin/components/components.sha1	Tue Feb 07 22:15:07 2017 +0100
+++ b/Admin/components/components.sha1	Wed Feb 08 21:04:18 2017 +0100
@@ -140,6 +140,7 @@
 5b19dc93082803b82aa553a5cfb3e914606c0ffd  polyml-5.6.tar.gz
 853ab0e9ff2b73790cc80a2d36cbff8b03e50a8e  polyml-test-7a7b742897e9.tar.gz
 c629cd499a724bbe37b962f727e4ff340c50299d  polyml-test-8529546198aa.tar.gz
+f132329ca1045858ef456cc08b197c9eeea6881b  postgresql-9.4.1212.tar.gz
 8ee375cfc38972f080dbc78f07b68dac03efe968  ProofGeneral-3.7.1.1.tar.gz
 847b52c0676b5eb0fbf0476f64fc08c2d72afd0c  ProofGeneral-4.1.tar.gz
 8e0b2b432755ef11d964e20637d1bc567d1c0477  ProofGeneral-4.2-1.tar.gz
diff -r f8f76a501d25 -r b28bd9dfe108 Admin/components/main
--- a/Admin/components/main	Tue Feb 07 22:15:07 2017 +0100
+++ b/Admin/components/main	Wed Feb 08 21:04:18 2017 +0100
@@ -11,6 +11,7 @@
 kodkodi-1.5.2
 nunchaku-0.3
 polyml-5.6-1
+postgresql-9.4.1212
 scala-2.11.8
 ssh-java-20161009
 spass-3.8ds
diff -r f8f76a501d25 -r b28bd9dfe108 src/Pure/General/postgresql.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/postgresql.scala	Wed Feb 08 21:04:18 2017 +0100
@@ -0,0 +1,41 @@
+/*  Title:      Pure/General/postgresql.scala
+    Author:     Makarius
+
+Support for PostgreSQL databases.
+*/
+
+package isabelle
+
+
+import java.sql.{DriverManager, Connection}
+
+
+object PostgreSQL
+{
+  /** database connection **/
+
+  val default_host = "localhost"
+  val default_port = 5432
+
+  def open_database(
+    user: String,
+    password: String,
+    database: String = "",
+    host: String = "",
+    port: Int = default_port): Database =
+  {
+    require(user != "")
+
+    val spec =
+      (if (host != "") host else "localhost") +
+      (if (port != default_port) ":" + port else "") + "/" +
+      (if (database != "") database else user)
+    val connection = DriverManager.getConnection("jdbc:postgresql://" + spec, user, password)
+    new Database(spec, connection)
+  }
+
+  class Database private[PostgreSQL](spec: String, val connection: Connection)
+  {
+    override def toString: String = spec
+  }
+}
diff -r f8f76a501d25 -r b28bd9dfe108 src/Pure/build-jars
--- a/src/Pure/build-jars	Tue Feb 07 22:15:07 2017 +0100
+++ b/src/Pure/build-jars	Wed Feb 08 21:04:18 2017 +0100
@@ -60,6 +60,7 @@
   General/output.scala
   General/path.scala
   General/position.scala
+  General/postgresql.scala
   General/pretty.scala
   General/properties.scala
   General/scan.scala