src/Pure/General/sql.scala
author wenzelm
Thu, 09 Mar 2023 12:54:19 +0100
changeset 77598 6370d9e5ab50
parent 77596 dd8b08729458
child 77664 f5d3ade80d15
permissions -rw-r--r--
proper support for Option[Date] columns;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
63788
3160826b92f8 clarified modules;
wenzelm
parents: 63784
diff changeset
     1
/*  Title:      Pure/General/sql.scala
63778
e06e899b78d0 clarified modules;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
e06e899b78d0 clarified modules;
wenzelm
parents:
diff changeset
     3
65006
632bdf7b8bab clarified modules;
wenzelm
parents: 65004
diff changeset
     4
Support for SQL databases: SQLite and PostgreSQL.
63778
e06e899b78d0 clarified modules;
wenzelm
parents:
diff changeset
     5
*/
e06e899b78d0 clarified modules;
wenzelm
parents:
diff changeset
     6
e06e899b78d0 clarified modules;
wenzelm
parents:
diff changeset
     7
package isabelle
e06e899b78d0 clarified modules;
wenzelm
parents:
diff changeset
     8
69393
ed0824ef337e static type for Library.using: avoid Java 11 warnings on "Illegal reflective access";
wenzelm
parents: 69327
diff changeset
     9
65021
da8ae577d171 clarified Date storage;
wenzelm
parents: 65020
diff changeset
    10
import java.time.OffsetDateTime
da8ae577d171 clarified Date storage;
wenzelm
parents: 65020
diff changeset
    11
import java.sql.{DriverManager, Connection, PreparedStatement, ResultSet}
63779
9da65bc75610 more operations;
wenzelm
parents: 63778
diff changeset
    12
77037
164a21e5d568 support specific connection types, for additional operations;
wenzelm
parents: 76870
diff changeset
    13
import org.sqlite.jdbc4.JDBC4Connection
77039
2f09dc0e6dda support IPC via database server;
wenzelm
parents: 77037
diff changeset
    14
import org.postgresql.{PGConnection, PGNotification}
77037
164a21e5d568 support specific connection types, for additional operations;
wenzelm
parents: 76870
diff changeset
    15
65740
83388f09e9ab clarified signature;
wenzelm
parents: 65739
diff changeset
    16
import scala.collection.mutable
83388f09e9ab clarified signature;
wenzelm
parents: 65739
diff changeset
    17
63779
9da65bc75610 more operations;
wenzelm
parents: 63778
diff changeset
    18
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73367
diff changeset
    19
object SQL {
65006
632bdf7b8bab clarified modules;
wenzelm
parents: 65004
diff changeset
    20
  /** SQL language **/
632bdf7b8bab clarified modules;
wenzelm
parents: 65004
diff changeset
    21
65730
7ae61e72a678 clarified signature;
wenzelm
parents: 65729
diff changeset
    22
  type Source = String
7ae61e72a678 clarified signature;
wenzelm
parents: 65729
diff changeset
    23
7ae61e72a678 clarified signature;
wenzelm
parents: 65729
diff changeset
    24
63778
e06e899b78d0 clarified modules;
wenzelm
parents:
diff changeset
    25
  /* concrete syntax */
e06e899b78d0 clarified modules;
wenzelm
parents:
diff changeset
    26
65321
2b1cd063e0b2 proper SQL syntax (according of PostgreSQL);
wenzelm
parents: 65319
diff changeset
    27
  def escape_char(c: Char): String =
63778
e06e899b78d0 clarified modules;
wenzelm
parents:
diff changeset
    28
    c match {
e06e899b78d0 clarified modules;
wenzelm
parents:
diff changeset
    29
      case '\u0000' => "\\0"
e06e899b78d0 clarified modules;
wenzelm
parents:
diff changeset
    30
      case '\'' => "\\'"
e06e899b78d0 clarified modules;
wenzelm
parents:
diff changeset
    31
      case '\"' => "\\\""
e06e899b78d0 clarified modules;
wenzelm
parents:
diff changeset
    32
      case '\b' => "\\b"
e06e899b78d0 clarified modules;
wenzelm
parents:
diff changeset
    33
      case '\n' => "\\n"
e06e899b78d0 clarified modules;
wenzelm
parents:
diff changeset
    34
      case '\r' => "\\r"
e06e899b78d0 clarified modules;
wenzelm
parents:
diff changeset
    35
      case '\t' => "\\t"
e06e899b78d0 clarified modules;
wenzelm
parents:
diff changeset
    36
      case '\u001a' => "\\Z"
e06e899b78d0 clarified modules;
wenzelm
parents:
diff changeset
    37
      case '\\' => "\\\\"
e06e899b78d0 clarified modules;
wenzelm
parents:
diff changeset
    38
      case _ => c.toString
e06e899b78d0 clarified modules;
wenzelm
parents:
diff changeset
    39
    }
e06e899b78d0 clarified modules;
wenzelm
parents:
diff changeset
    40
65730
7ae61e72a678 clarified signature;
wenzelm
parents: 65729
diff changeset
    41
  def string(s: String): Source =
71601
97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA;
wenzelm
parents: 69980
diff changeset
    42
    s.iterator.map(escape_char).mkString("'", "", "'")
63778
e06e899b78d0 clarified modules;
wenzelm
parents:
diff changeset
    43
65730
7ae61e72a678 clarified signature;
wenzelm
parents: 65729
diff changeset
    44
  def ident(s: String): Source =
65677
7d25b8dbdbfa proper quote (amending 546020a98a91): e.g. relevant for "ISABELLE_BUILD_OPTIONS";
wenzelm
parents: 65673
diff changeset
    45
    Long_Name.implode(Long_Name.explode(s).map(a => quote(a.replace("\"", "\"\""))))
63779
9da65bc75610 more operations;
wenzelm
parents: 63778
diff changeset
    46
65730
7ae61e72a678 clarified signature;
wenzelm
parents: 65729
diff changeset
    47
  def enclose(s: Source): Source = "(" + s + ")"
7ae61e72a678 clarified signature;
wenzelm
parents: 65729
diff changeset
    48
  def enclosure(ss: Iterable[Source]): Source = ss.mkString("(", ", ", ")")
63791
c6cbdfaae19e more operations;
wenzelm
parents: 63790
diff changeset
    49
77381
a86e346b20d8 misc tuning and clarification: more uniform use of optional "sql" in SQL.Table.delete/select;
wenzelm
parents: 77377
diff changeset
    50
  def separate(sql: Source): Source =
a86e346b20d8 misc tuning and clarification: more uniform use of optional "sql" in SQL.Table.delete/select;
wenzelm
parents: 77377
diff changeset
    51
    (if (sql.isEmpty || sql.startsWith(" ")) "" else " ") + sql
a86e346b20d8 misc tuning and clarification: more uniform use of optional "sql" in SQL.Table.delete/select;
wenzelm
parents: 77377
diff changeset
    52
77403
be8e14c7da80 clarified signature, although "sql" argument is de-facto mandatory;
wenzelm
parents: 77381
diff changeset
    53
  def select(columns: List[Column] = Nil, distinct: Boolean = false, sql: Source = ""): Source =
65774
1001fb86d7f7 clarified signature;
wenzelm
parents: 65748
diff changeset
    54
    "SELECT " + (if (distinct) "DISTINCT " else "") +
77403
be8e14c7da80 clarified signature, although "sql" argument is de-facto mandatory;
wenzelm
parents: 77381
diff changeset
    55
    (if (columns.isEmpty) "*" else commas(columns.map(_.ident))) + " FROM " + sql
65644
7ef438495a02 support for qualified names, which are not quoted (e.g. for SQLite);
wenzelm
parents: 65641
diff changeset
    56
65775
123f2c0995b8 tuned signature;
wenzelm
parents: 65774
diff changeset
    57
  val join_outer: Source = " LEFT OUTER JOIN "
123f2c0995b8 tuned signature;
wenzelm
parents: 65774
diff changeset
    58
  val join_inner: Source = " INNER JOIN "
65776
373d708898d4 tuned signature;
wenzelm
parents: 65775
diff changeset
    59
  def join(outer: Boolean): Source = if (outer) join_outer else join_inner
65775
123f2c0995b8 tuned signature;
wenzelm
parents: 65774
diff changeset
    60
77370
47c2ac81ddd4 clarified signature: more robust operations;
wenzelm
parents: 77368
diff changeset
    61
  def infix(op: Source, args: Iterable[Source]): Source = {
47c2ac81ddd4 clarified signature: more robust operations;
wenzelm
parents: 77368
diff changeset
    62
    val body = args.iterator.filter(_.nonEmpty).mkString(" " + op + " ")
47c2ac81ddd4 clarified signature: more robust operations;
wenzelm
parents: 77368
diff changeset
    63
    if_proper(body, enclose(body))
47c2ac81ddd4 clarified signature: more robust operations;
wenzelm
parents: 77368
diff changeset
    64
  }
47c2ac81ddd4 clarified signature: more robust operations;
wenzelm
parents: 77368
diff changeset
    65
47c2ac81ddd4 clarified signature: more robust operations;
wenzelm
parents: 77368
diff changeset
    66
  def AND(args: Iterable[Source]): Source = infix("AND", args)
47c2ac81ddd4 clarified signature: more robust operations;
wenzelm
parents: 77368
diff changeset
    67
  def OR(args: Iterable[Source]): Source = infix("OR", args)
47c2ac81ddd4 clarified signature: more robust operations;
wenzelm
parents: 77368
diff changeset
    68
47c2ac81ddd4 clarified signature: more robust operations;
wenzelm
parents: 77368
diff changeset
    69
  def and(args: Source*): Source = AND(args)
47c2ac81ddd4 clarified signature: more robust operations;
wenzelm
parents: 77368
diff changeset
    70
  def or(args: Source*): Source = OR(args)
47c2ac81ddd4 clarified signature: more robust operations;
wenzelm
parents: 77368
diff changeset
    71
47c2ac81ddd4 clarified signature: more robust operations;
wenzelm
parents: 77368
diff changeset
    72
  val TRUE: Source = "TRUE"
47c2ac81ddd4 clarified signature: more robust operations;
wenzelm
parents: 77368
diff changeset
    73
  val FALSE: Source = "FALSE"
47c2ac81ddd4 clarified signature: more robust operations;
wenzelm
parents: 77368
diff changeset
    74
77375
324f5821a4a4 clarified signature: more concise operations;
wenzelm
parents: 77370
diff changeset
    75
  def equal(sql: Source, s: String): Source = sql + " = " + string(s)
324f5821a4a4 clarified signature: more concise operations;
wenzelm
parents: 77370
diff changeset
    76
324f5821a4a4 clarified signature: more concise operations;
wenzelm
parents: 77370
diff changeset
    77
  def member(sql: Source, set: Iterable[String]): Source =
77370
47c2ac81ddd4 clarified signature: more robust operations;
wenzelm
parents: 77368
diff changeset
    78
    if (set.isEmpty) FALSE
77375
324f5821a4a4 clarified signature: more concise operations;
wenzelm
parents: 77370
diff changeset
    79
    else OR(set.iterator.map(equal(sql, _)).toList)
65804
wenzelm
parents: 65780
diff changeset
    80
77370
47c2ac81ddd4 clarified signature: more robust operations;
wenzelm
parents: 77368
diff changeset
    81
  def where(sql: Source): Source = if_proper(sql, " WHERE " + sql)
47c2ac81ddd4 clarified signature: more robust operations;
wenzelm
parents: 77368
diff changeset
    82
47c2ac81ddd4 clarified signature: more robust operations;
wenzelm
parents: 77368
diff changeset
    83
65008
ed2eedf786f3 clarified handling of SQL.Type;
wenzelm
parents: 65007
diff changeset
    84
  /* types */
ed2eedf786f3 clarified handling of SQL.Type;
wenzelm
parents: 65007
diff changeset
    85
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73367
diff changeset
    86
  object Type extends Enumeration {
65011
42bffd1637f0 support for type Boolean;
wenzelm
parents: 65010
diff changeset
    87
    val Boolean = Value("BOOLEAN")
65008
ed2eedf786f3 clarified handling of SQL.Type;
wenzelm
parents: 65007
diff changeset
    88
    val Int = Value("INTEGER")
ed2eedf786f3 clarified handling of SQL.Type;
wenzelm
parents: 65007
diff changeset
    89
    val Long = Value("BIGINT")
ed2eedf786f3 clarified handling of SQL.Type;
wenzelm
parents: 65007
diff changeset
    90
    val Double = Value("DOUBLE PRECISION")
ed2eedf786f3 clarified handling of SQL.Type;
wenzelm
parents: 65007
diff changeset
    91
    val String = Value("TEXT")
ed2eedf786f3 clarified handling of SQL.Type;
wenzelm
parents: 65007
diff changeset
    92
    val Bytes = Value("BLOB")
65014
97a622d01609 support for type Date;
wenzelm
parents: 65013
diff changeset
    93
    val Date = Value("TIMESTAMP WITH TIME ZONE")
65008
ed2eedf786f3 clarified handling of SQL.Type;
wenzelm
parents: 65007
diff changeset
    94
  }
ed2eedf786f3 clarified handling of SQL.Type;
wenzelm
parents: 65007
diff changeset
    95
65730
7ae61e72a678 clarified signature;
wenzelm
parents: 65729
diff changeset
    96
  def sql_type_default(T: Type.Value): Source = T.toString
65013
wenzelm
parents: 65012
diff changeset
    97
65730
7ae61e72a678 clarified signature;
wenzelm
parents: 65729
diff changeset
    98
  def sql_type_sqlite(T: Type.Value): Source =
65019
0ca91e5d52df tuned signature;
wenzelm
parents: 65018
diff changeset
    99
    if (T == Type.Boolean) "INTEGER"
0ca91e5d52df tuned signature;
wenzelm
parents: 65018
diff changeset
   100
    else if (T == Type.Date) "TEXT"
0ca91e5d52df tuned signature;
wenzelm
parents: 65018
diff changeset
   101
    else sql_type_default(T)
65013
wenzelm
parents: 65012
diff changeset
   102
65730
7ae61e72a678 clarified signature;
wenzelm
parents: 65729
diff changeset
   103
  def sql_type_postgresql(T: Type.Value): Source =
65019
0ca91e5d52df tuned signature;
wenzelm
parents: 65018
diff changeset
   104
    if (T == Type.Bytes) "BYTEA"
0ca91e5d52df tuned signature;
wenzelm
parents: 65018
diff changeset
   105
    else sql_type_default(T)
65008
ed2eedf786f3 clarified handling of SQL.Type;
wenzelm
parents: 65007
diff changeset
   106
ed2eedf786f3 clarified handling of SQL.Type;
wenzelm
parents: 65007
diff changeset
   107
63779
9da65bc75610 more operations;
wenzelm
parents: 63778
diff changeset
   108
  /* columns */
9da65bc75610 more operations;
wenzelm
parents: 63778
diff changeset
   109
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73367
diff changeset
   110
  object Column {
65280
ef37f5236794 prefer non-strict default;
wenzelm
parents: 65022
diff changeset
   111
    def bool(name: String, strict: Boolean = false, primary_key: Boolean = false): Column =
65018
8b36f225bbee clarified signature;
wenzelm
parents: 65014
diff changeset
   112
      Column(name, Type.Boolean, strict, primary_key)
65280
ef37f5236794 prefer non-strict default;
wenzelm
parents: 65022
diff changeset
   113
    def int(name: String, strict: Boolean = false, primary_key: Boolean = false): Column =
65018
8b36f225bbee clarified signature;
wenzelm
parents: 65014
diff changeset
   114
      Column(name, Type.Int, strict, primary_key)
65280
ef37f5236794 prefer non-strict default;
wenzelm
parents: 65022
diff changeset
   115
    def long(name: String, strict: Boolean = false, primary_key: Boolean = false): Column =
65018
8b36f225bbee clarified signature;
wenzelm
parents: 65014
diff changeset
   116
      Column(name, Type.Long, strict, primary_key)
65280
ef37f5236794 prefer non-strict default;
wenzelm
parents: 65022
diff changeset
   117
    def double(name: String, strict: Boolean = false, primary_key: Boolean = false): Column =
65018
8b36f225bbee clarified signature;
wenzelm
parents: 65014
diff changeset
   118
      Column(name, Type.Double, strict, primary_key)
65280
ef37f5236794 prefer non-strict default;
wenzelm
parents: 65022
diff changeset
   119
    def string(name: String, strict: Boolean = false, primary_key: Boolean = false): Column =
65018
8b36f225bbee clarified signature;
wenzelm
parents: 65014
diff changeset
   120
      Column(name, Type.String, strict, primary_key)
65280
ef37f5236794 prefer non-strict default;
wenzelm
parents: 65022
diff changeset
   121
    def bytes(name: String, strict: Boolean = false, primary_key: Boolean = false): Column =
65018
8b36f225bbee clarified signature;
wenzelm
parents: 65014
diff changeset
   122
      Column(name, Type.Bytes, strict, primary_key)
65280
ef37f5236794 prefer non-strict default;
wenzelm
parents: 65022
diff changeset
   123
    def date(name: String, strict: Boolean = false, primary_key: Boolean = false): Column =
65018
8b36f225bbee clarified signature;
wenzelm
parents: 65014
diff changeset
   124
      Column(name, Type.Date, strict, primary_key)
63779
9da65bc75610 more operations;
wenzelm
parents: 63778
diff changeset
   125
  }
9da65bc75610 more operations;
wenzelm
parents: 63778
diff changeset
   126
65018
8b36f225bbee clarified signature;
wenzelm
parents: 65014
diff changeset
   127
  sealed case class Column(
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73367
diff changeset
   128
    name: String,
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73367
diff changeset
   129
    T: Type.Value,
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73367
diff changeset
   130
    strict: Boolean = false,
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73367
diff changeset
   131
    primary_key: Boolean = false,
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73367
diff changeset
   132
    expr: SQL.Source = ""
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73367
diff changeset
   133
  ) {
66857
f8f42289c4df tuned signature;
wenzelm
parents: 66856
diff changeset
   134
    def make_primary_key: Column = copy(primary_key = true)
f8f42289c4df tuned signature;
wenzelm
parents: 66856
diff changeset
   135
65691
2229276a1f99 eliminated redundant type SQL.View;
wenzelm
parents: 65690
diff changeset
   136
    def apply(table: Table): Column =
2229276a1f99 eliminated redundant type SQL.View;
wenzelm
parents: 65690
diff changeset
   137
      Column(Long_Name.qualify(table.name, name), T, strict = strict, primary_key = primary_key)
65644
7ef438495a02 support for qualified names, which are not quoted (e.g. for SQLite);
wenzelm
parents: 65641
diff changeset
   138
65780
8baf789b1537 allow column with defining expression;
wenzelm
parents: 65778
diff changeset
   139
    def ident: Source =
8baf789b1537 allow column with defining expression;
wenzelm
parents: 65778
diff changeset
   140
      if (expr == "") SQL.ident(name)
8baf789b1537 allow column with defining expression;
wenzelm
parents: 65778
diff changeset
   141
      else enclose(expr) + " AS " + SQL.ident(name)
65695
4edac706bc5e tuned signature;
wenzelm
parents: 65691
diff changeset
   142
65730
7ae61e72a678 clarified signature;
wenzelm
parents: 65729
diff changeset
   143
    def decl(sql_type: Type.Value => Source): Source =
65695
4edac706bc5e tuned signature;
wenzelm
parents: 65691
diff changeset
   144
      ident + " " + sql_type(T) + (if (strict || primary_key) " NOT NULL" else "")
63781
af9fe0b6b78e support for (single) primary key;
wenzelm
parents: 63780
diff changeset
   145
66856
6b90c688a6dc tuned signature;
wenzelm
parents: 65918
diff changeset
   146
    def defined: String = ident + " IS NOT NULL"
6b90c688a6dc tuned signature;
wenzelm
parents: 65918
diff changeset
   147
    def undefined: String = ident + " IS NULL"
6b90c688a6dc tuned signature;
wenzelm
parents: 65918
diff changeset
   148
77375
324f5821a4a4 clarified signature: more concise operations;
wenzelm
parents: 77370
diff changeset
   149
    def equal(s: String): Source = SQL.equal(ident, s)
324f5821a4a4 clarified signature: more concise operations;
wenzelm
parents: 77370
diff changeset
   150
    def member(set: Iterable[String]): Source = SQL.member(ident, set)
324f5821a4a4 clarified signature: more concise operations;
wenzelm
parents: 77370
diff changeset
   151
324f5821a4a4 clarified signature: more concise operations;
wenzelm
parents: 77370
diff changeset
   152
    def where_equal(s: String): Source = SQL.where(equal(s))
324f5821a4a4 clarified signature: more concise operations;
wenzelm
parents: 77370
diff changeset
   153
    def where_member(set: Iterable[String]): Source = SQL.where(member(set))
65593
607f7ad07a60 tuned signature;
wenzelm
parents: 65327
diff changeset
   154
65730
7ae61e72a678 clarified signature;
wenzelm
parents: 65729
diff changeset
   155
    override def toString: Source = ident
63779
9da65bc75610 more operations;
wenzelm
parents: 63778
diff changeset
   156
  }
9da65bc75610 more operations;
wenzelm
parents: 63778
diff changeset
   157
76870
c6cdf2a641f4 clarified signature: more explicit types;
wenzelm
parents: 76529
diff changeset
   158
  def order_by(columns: List[Column], descending: Boolean = false): Source =
c6cdf2a641f4 clarified signature: more explicit types;
wenzelm
parents: 76529
diff changeset
   159
    " ORDER BY " + columns.mkString(", ") + (if (descending) " DESC" else "")
c6cdf2a641f4 clarified signature: more explicit types;
wenzelm
parents: 76529
diff changeset
   160
63780
163244cefb4e more operations;
wenzelm
parents: 63779
diff changeset
   161
163244cefb4e more operations;
wenzelm
parents: 63779
diff changeset
   162
  /* tables */
163244cefb4e more operations;
wenzelm
parents: 63779
diff changeset
   163
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73367
diff changeset
   164
  sealed case class Table(name: String, columns: List[Column], body: Source = "") {
63781
af9fe0b6b78e support for (single) primary key;
wenzelm
parents: 63780
diff changeset
   165
    Library.duplicates(columns.map(_.name)) match {
af9fe0b6b78e support for (single) primary key;
wenzelm
parents: 63780
diff changeset
   166
      case Nil =>
af9fe0b6b78e support for (single) primary key;
wenzelm
parents: 63780
diff changeset
   167
      case bad => error("Duplicate column names " + commas_quote(bad) + " for table " + quote(name))
af9fe0b6b78e support for (single) primary key;
wenzelm
parents: 63780
diff changeset
   168
    }
af9fe0b6b78e support for (single) primary key;
wenzelm
parents: 63780
diff changeset
   169
65730
7ae61e72a678 clarified signature;
wenzelm
parents: 65729
diff changeset
   170
    def ident: Source = SQL.ident(name)
65691
2229276a1f99 eliminated redundant type SQL.View;
wenzelm
parents: 65690
diff changeset
   171
65730
7ae61e72a678 clarified signature;
wenzelm
parents: 65729
diff changeset
   172
    def query: Source =
65696
3f53a05c1266 tuned signature;
wenzelm
parents: 65695
diff changeset
   173
      if (body == "") error("Missing SQL body for table " + quote(name))
3f53a05c1266 tuned signature;
wenzelm
parents: 65695
diff changeset
   174
      else SQL.enclose(body)
65649
0818da4f67bb tuned signature;
wenzelm
parents: 65648
diff changeset
   175
65778
666a1bac126b tuned signature;
wenzelm
parents: 65776
diff changeset
   176
    def query_named: Source = query + " AS " + SQL.ident(name)
65702
7c6a91deb212 tuned signature;
wenzelm
parents: 65701
diff changeset
   177
75966
ed29a23e8b62 tuned signature;
wenzelm
parents: 75965
diff changeset
   178
    def create(strict: Boolean, sql_type: Type.Value => Source): Source = {
65325
981df08de0ab more general primary_key;
wenzelm
parents: 65323
diff changeset
   179
      val primary_key =
981df08de0ab more general primary_key;
wenzelm
parents: 65323
diff changeset
   180
        columns.filter(_.primary_key).map(_.name) match {
981df08de0ab more general primary_key;
wenzelm
parents: 65323
diff changeset
   181
          case Nil => Nil
981df08de0ab more general primary_key;
wenzelm
parents: 65323
diff changeset
   182
          case keys => List("PRIMARY KEY " + enclosure(keys))
981df08de0ab more general primary_key;
wenzelm
parents: 65323
diff changeset
   183
        }
65701
d788c11176e5 simplified: standard toString is SQL.ident;
wenzelm
parents: 65699
diff changeset
   184
      "CREATE TABLE " + (if (strict) "" else "IF NOT EXISTS ") +
d788c11176e5 simplified: standard toString is SQL.ident;
wenzelm
parents: 65699
diff changeset
   185
        ident + " " + enclosure(columns.map(_.decl(sql_type)) ::: primary_key)
63781
af9fe0b6b78e support for (single) primary key;
wenzelm
parents: 63780
diff changeset
   186
    }
af9fe0b6b78e support for (single) primary key;
wenzelm
parents: 63780
diff changeset
   187
65698
38139b2067cf clarified signature;
wenzelm
parents: 65697
diff changeset
   188
    def create_index(index_name: String, index_columns: List[Column],
65730
7ae61e72a678 clarified signature;
wenzelm
parents: 65729
diff changeset
   189
        strict: Boolean = false, unique: Boolean = false): Source =
63791
c6cbdfaae19e more operations;
wenzelm
parents: 63790
diff changeset
   190
      "CREATE " + (if (unique) "UNIQUE " else "") + "INDEX " +
65695
4edac706bc5e tuned signature;
wenzelm
parents: 65691
diff changeset
   191
        (if (strict) "" else "IF NOT EXISTS ") + SQL.ident(index_name) + " ON " +
4edac706bc5e tuned signature;
wenzelm
parents: 65691
diff changeset
   192
        ident + " " + enclosure(index_columns.map(_.name))
63791
c6cbdfaae19e more operations;
wenzelm
parents: 63790
diff changeset
   193
77365
a10fa2112854 clarified signature;
wenzelm
parents: 77364
diff changeset
   194
    def insert_cmd(cmd: Source = "INSERT", sql: Source = ""): Source =
77377
82fdc7cf9d44 tuned whitespace in generated SQL;
wenzelm
parents: 77375
diff changeset
   195
      cmd + " INTO " + ident + " VALUES " + enclosure(columns.map(_ => "?")) + SQL.separate(sql)
63791
c6cbdfaae19e more operations;
wenzelm
parents: 63790
diff changeset
   196
77365
a10fa2112854 clarified signature;
wenzelm
parents: 77364
diff changeset
   197
    def insert(sql: Source = ""): Source = insert_cmd(sql = sql)
65703
cead65c19f2e more direct insert_permissive statement, which avoids somewhat fragile nested transactions;
wenzelm
parents: 65702
diff changeset
   198
65730
7ae61e72a678 clarified signature;
wenzelm
parents: 65729
diff changeset
   199
    def delete(sql: Source = ""): Source =
77377
82fdc7cf9d44 tuned whitespace in generated SQL;
wenzelm
parents: 77375
diff changeset
   200
      "DELETE FROM " + ident + SQL.separate(sql)
65319
64da14387b2c more operations;
wenzelm
parents: 65292
diff changeset
   201
77537
1bbf29ec9ce3 more operations;
wenzelm
parents: 77527
diff changeset
   202
    def update(update_columns: List[Column] = Nil, sql: Source = ""): Source =
1bbf29ec9ce3 more operations;
wenzelm
parents: 77527
diff changeset
   203
      "UPDATE " + ident + " SET " + commas(update_columns.map(c => c.ident + " = ?")) +
1bbf29ec9ce3 more operations;
wenzelm
parents: 77527
diff changeset
   204
        SQL.separate(sql)
1bbf29ec9ce3 more operations;
wenzelm
parents: 77527
diff changeset
   205
65774
1001fb86d7f7 clarified signature;
wenzelm
parents: 65748
diff changeset
   206
    def select(
77381
a86e346b20d8 misc tuning and clarification: more uniform use of optional "sql" in SQL.Table.delete/select;
wenzelm
parents: 77377
diff changeset
   207
      select_columns: List[Column] = Nil,
a86e346b20d8 misc tuning and clarification: more uniform use of optional "sql" in SQL.Table.delete/select;
wenzelm
parents: 77377
diff changeset
   208
      distinct: Boolean = false,
a86e346b20d8 misc tuning and clarification: more uniform use of optional "sql" in SQL.Table.delete/select;
wenzelm
parents: 77377
diff changeset
   209
      sql: Source = ""
77403
be8e14c7da80 clarified signature, although "sql" argument is de-facto mandatory;
wenzelm
parents: 77381
diff changeset
   210
    ): Source = SQL.select(select_columns, distinct = distinct, sql = ident + SQL.separate(sql))
63790
3d723062dc70 more operations;
wenzelm
parents: 63788
diff changeset
   211
65730
7ae61e72a678 clarified signature;
wenzelm
parents: 65729
diff changeset
   212
    override def toString: Source = ident
63780
163244cefb4e more operations;
wenzelm
parents: 63779
diff changeset
   213
  }
63790
3d723062dc70 more operations;
wenzelm
parents: 63788
diff changeset
   214
3d723062dc70 more operations;
wenzelm
parents: 63788
diff changeset
   215
77596
dd8b08729458 clarified signature;
wenzelm
parents: 77591
diff changeset
   216
  /* table groups */
dd8b08729458 clarified signature;
wenzelm
parents: 77591
diff changeset
   217
dd8b08729458 clarified signature;
wenzelm
parents: 77591
diff changeset
   218
  object Tables {
dd8b08729458 clarified signature;
wenzelm
parents: 77591
diff changeset
   219
    def list(list: List[Table]): Tables = new Tables(list)
dd8b08729458 clarified signature;
wenzelm
parents: 77591
diff changeset
   220
    def apply(args: Table*): Tables = list(args.toList)
dd8b08729458 clarified signature;
wenzelm
parents: 77591
diff changeset
   221
  }
dd8b08729458 clarified signature;
wenzelm
parents: 77591
diff changeset
   222
dd8b08729458 clarified signature;
wenzelm
parents: 77591
diff changeset
   223
  final class Tables private(val list: List[Table]) extends Iterable[Table] {
dd8b08729458 clarified signature;
wenzelm
parents: 77591
diff changeset
   224
    override def toString: String = list.mkString("SQL.Tables(", ", ", ")")
dd8b08729458 clarified signature;
wenzelm
parents: 77591
diff changeset
   225
dd8b08729458 clarified signature;
wenzelm
parents: 77591
diff changeset
   226
    def iterator: Iterator[Table] = list.iterator
dd8b08729458 clarified signature;
wenzelm
parents: 77591
diff changeset
   227
dd8b08729458 clarified signature;
wenzelm
parents: 77591
diff changeset
   228
    // requires transaction
dd8b08729458 clarified signature;
wenzelm
parents: 77591
diff changeset
   229
    def create_lock(db: Database): Unit = {
dd8b08729458 clarified signature;
wenzelm
parents: 77591
diff changeset
   230
      foreach(db.create_table(_))
dd8b08729458 clarified signature;
wenzelm
parents: 77591
diff changeset
   231
      lock(db)
dd8b08729458 clarified signature;
wenzelm
parents: 77591
diff changeset
   232
    }
dd8b08729458 clarified signature;
wenzelm
parents: 77591
diff changeset
   233
dd8b08729458 clarified signature;
wenzelm
parents: 77591
diff changeset
   234
    // requires transaction
dd8b08729458 clarified signature;
wenzelm
parents: 77591
diff changeset
   235
    def lock(db: Database): Unit = {
dd8b08729458 clarified signature;
wenzelm
parents: 77591
diff changeset
   236
      val sql = db.lock_tables(list)
dd8b08729458 clarified signature;
wenzelm
parents: 77591
diff changeset
   237
      if (sql.nonEmpty) db.execute_statement(sql)
dd8b08729458 clarified signature;
wenzelm
parents: 77591
diff changeset
   238
    }
dd8b08729458 clarified signature;
wenzelm
parents: 77591
diff changeset
   239
  }
dd8b08729458 clarified signature;
wenzelm
parents: 77591
diff changeset
   240
dd8b08729458 clarified signature;
wenzelm
parents: 77591
diff changeset
   241
65012
wenzelm
parents: 65011
diff changeset
   242
wenzelm
parents: 65011
diff changeset
   243
  /** SQL database operations **/
wenzelm
parents: 65011
diff changeset
   244
65740
83388f09e9ab clarified signature;
wenzelm
parents: 65739
diff changeset
   245
  /* statements */
83388f09e9ab clarified signature;
wenzelm
parents: 65739
diff changeset
   246
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73367
diff changeset
   247
  class Statement private[SQL](val db: Database, val rep: PreparedStatement) extends AutoCloseable {
65740
83388f09e9ab clarified signature;
wenzelm
parents: 65739
diff changeset
   248
    stmt =>
83388f09e9ab clarified signature;
wenzelm
parents: 65739
diff changeset
   249
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73367
diff changeset
   250
    object bool {
73340
0ffcad1f6130 tuned --- fewer warnings;
wenzelm
parents: 73337
diff changeset
   251
      def update(i: Int, x: Boolean): Unit = rep.setBoolean(i, x)
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73367
diff changeset
   252
      def update(i: Int, x: Option[Boolean]): Unit = {
65748
1f4a80e80c88 tuned signature;
wenzelm
parents: 65741
diff changeset
   253
        if (x.isDefined) update(i, x.get)
1f4a80e80c88 tuned signature;
wenzelm
parents: 65741
diff changeset
   254
        else rep.setNull(i, java.sql.Types.BOOLEAN)
1f4a80e80c88 tuned signature;
wenzelm
parents: 65741
diff changeset
   255
      }
65740
83388f09e9ab clarified signature;
wenzelm
parents: 65739
diff changeset
   256
    }
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73367
diff changeset
   257
    object int {
73340
0ffcad1f6130 tuned --- fewer warnings;
wenzelm
parents: 73337
diff changeset
   258
      def update(i: Int, x: Int): Unit = rep.setInt(i, x)
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73367
diff changeset
   259
      def update(i: Int, x: Option[Int]): Unit = {
65748
1f4a80e80c88 tuned signature;
wenzelm
parents: 65741
diff changeset
   260
        if (x.isDefined) update(i, x.get)
1f4a80e80c88 tuned signature;
wenzelm
parents: 65741
diff changeset
   261
        else rep.setNull(i, java.sql.Types.INTEGER)
1f4a80e80c88 tuned signature;
wenzelm
parents: 65741
diff changeset
   262
      }
65740
83388f09e9ab clarified signature;
wenzelm
parents: 65739
diff changeset
   263
    }
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73367
diff changeset
   264
    object long {
73340
0ffcad1f6130 tuned --- fewer warnings;
wenzelm
parents: 73337
diff changeset
   265
      def update(i: Int, x: Long): Unit = rep.setLong(i, x)
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73367
diff changeset
   266
      def update(i: Int, x: Option[Long]): Unit = {
65748
1f4a80e80c88 tuned signature;
wenzelm
parents: 65741
diff changeset
   267
        if (x.isDefined) update(i, x.get)
1f4a80e80c88 tuned signature;
wenzelm
parents: 65741
diff changeset
   268
        else rep.setNull(i, java.sql.Types.BIGINT)
1f4a80e80c88 tuned signature;
wenzelm
parents: 65741
diff changeset
   269
      }
65740
83388f09e9ab clarified signature;
wenzelm
parents: 65739
diff changeset
   270
    }
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73367
diff changeset
   271
    object double {
73340
0ffcad1f6130 tuned --- fewer warnings;
wenzelm
parents: 73337
diff changeset
   272
      def update(i: Int, x: Double): Unit = rep.setDouble(i, x)
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73367
diff changeset
   273
      def update(i: Int, x: Option[Double]): Unit = {
65748
1f4a80e80c88 tuned signature;
wenzelm
parents: 65741
diff changeset
   274
        if (x.isDefined) update(i, x.get)
1f4a80e80c88 tuned signature;
wenzelm
parents: 65741
diff changeset
   275
        else rep.setNull(i, java.sql.Types.DOUBLE)
1f4a80e80c88 tuned signature;
wenzelm
parents: 65741
diff changeset
   276
      }
1f4a80e80c88 tuned signature;
wenzelm
parents: 65741
diff changeset
   277
    }
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73367
diff changeset
   278
    object string {
73340
0ffcad1f6130 tuned --- fewer warnings;
wenzelm
parents: 73337
diff changeset
   279
      def update(i: Int, x: String): Unit = rep.setString(i, x)
65748
1f4a80e80c88 tuned signature;
wenzelm
parents: 65741
diff changeset
   280
      def update(i: Int, x: Option[String]): Unit = update(i, x.orNull)
65740
83388f09e9ab clarified signature;
wenzelm
parents: 65739
diff changeset
   281
    }
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73367
diff changeset
   282
    object bytes {
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73367
diff changeset
   283
      def update(i: Int, bytes: Bytes): Unit = {
65748
1f4a80e80c88 tuned signature;
wenzelm
parents: 65741
diff changeset
   284
        if (bytes == null) rep.setBytes(i, null)
1f4a80e80c88 tuned signature;
wenzelm
parents: 65741
diff changeset
   285
        else rep.setBinaryStream(i, bytes.stream(), bytes.length)
1f4a80e80c88 tuned signature;
wenzelm
parents: 65741
diff changeset
   286
      }
1f4a80e80c88 tuned signature;
wenzelm
parents: 65741
diff changeset
   287
      def update(i: Int, bytes: Option[Bytes]): Unit = update(i, bytes.orNull)
65740
83388f09e9ab clarified signature;
wenzelm
parents: 65739
diff changeset
   288
    }
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73367
diff changeset
   289
    object date {
65748
1f4a80e80c88 tuned signature;
wenzelm
parents: 65741
diff changeset
   290
      def update(i: Int, date: Date): Unit = db.update_date(stmt, i, date)
1f4a80e80c88 tuned signature;
wenzelm
parents: 65741
diff changeset
   291
      def update(i: Int, date: Option[Date]): Unit = update(i, date.orNull)
1f4a80e80c88 tuned signature;
wenzelm
parents: 65741
diff changeset
   292
    }
65740
83388f09e9ab clarified signature;
wenzelm
parents: 65739
diff changeset
   293
83388f09e9ab clarified signature;
wenzelm
parents: 65739
diff changeset
   294
    def execute(): Boolean = rep.execute()
83388f09e9ab clarified signature;
wenzelm
parents: 65739
diff changeset
   295
    def execute_query(): Result = new Result(this, rep.executeQuery())
83388f09e9ab clarified signature;
wenzelm
parents: 65739
diff changeset
   296
73367
77ef8bef0593 clarified signature --- fewer warnings;
wenzelm
parents: 73340
diff changeset
   297
    def close(): Unit = rep.close()
65740
83388f09e9ab clarified signature;
wenzelm
parents: 65739
diff changeset
   298
  }
83388f09e9ab clarified signature;
wenzelm
parents: 65739
diff changeset
   299
83388f09e9ab clarified signature;
wenzelm
parents: 65739
diff changeset
   300
63790
3d723062dc70 more operations;
wenzelm
parents: 63788
diff changeset
   301
  /* results */
3d723062dc70 more operations;
wenzelm
parents: 63788
diff changeset
   302
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73367
diff changeset
   303
  class Result private[SQL](val stmt: Statement, val rep: ResultSet) {
65740
83388f09e9ab clarified signature;
wenzelm
parents: 65739
diff changeset
   304
    res =>
83388f09e9ab clarified signature;
wenzelm
parents: 65739
diff changeset
   305
83388f09e9ab clarified signature;
wenzelm
parents: 65739
diff changeset
   306
    def next(): Boolean = rep.next()
83388f09e9ab clarified signature;
wenzelm
parents: 65739
diff changeset
   307
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73367
diff changeset
   308
    def iterator[A](get: Result => A): Iterator[A] = new Iterator[A] {
65740
83388f09e9ab clarified signature;
wenzelm
parents: 65739
diff changeset
   309
      private var _next: Boolean = res.next()
83388f09e9ab clarified signature;
wenzelm
parents: 65739
diff changeset
   310
      def hasNext: Boolean = _next
73337
0af9e7e4476f tuned --- fewer warnings;
wenzelm
parents: 71601
diff changeset
   311
      def next(): A = { val x = get(res); _next = res.next(); x }
65740
83388f09e9ab clarified signature;
wenzelm
parents: 65739
diff changeset
   312
    }
83388f09e9ab clarified signature;
wenzelm
parents: 65739
diff changeset
   313
83388f09e9ab clarified signature;
wenzelm
parents: 65739
diff changeset
   314
    def bool(column: Column): Boolean = rep.getBoolean(column.name)
83388f09e9ab clarified signature;
wenzelm
parents: 65739
diff changeset
   315
    def int(column: Column): Int = rep.getInt(column.name)
83388f09e9ab clarified signature;
wenzelm
parents: 65739
diff changeset
   316
    def long(column: Column): Long = rep.getLong(column.name)
83388f09e9ab clarified signature;
wenzelm
parents: 65739
diff changeset
   317
    def double(column: Column): Double = rep.getDouble(column.name)
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73367
diff changeset
   318
    def string(column: Column): String = {
65740
83388f09e9ab clarified signature;
wenzelm
parents: 65739
diff changeset
   319
      val s = rep.getString(column.name)
83388f09e9ab clarified signature;
wenzelm
parents: 65739
diff changeset
   320
      if (s == null) "" else s
83388f09e9ab clarified signature;
wenzelm
parents: 65739
diff changeset
   321
    }
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73367
diff changeset
   322
    def bytes(column: Column): Bytes = {
65740
83388f09e9ab clarified signature;
wenzelm
parents: 65739
diff changeset
   323
      val bs = rep.getBytes(column.name)
83388f09e9ab clarified signature;
wenzelm
parents: 65739
diff changeset
   324
      if (bs == null) Bytes.empty else Bytes(bs)
83388f09e9ab clarified signature;
wenzelm
parents: 65739
diff changeset
   325
    }
83388f09e9ab clarified signature;
wenzelm
parents: 65739
diff changeset
   326
    def date(column: Column): Date = stmt.db.date(res, column)
83388f09e9ab clarified signature;
wenzelm
parents: 65739
diff changeset
   327
71601
97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA;
wenzelm
parents: 69980
diff changeset
   328
    def timing(c1: Column, c2: Column, c3: Column): Timing =
65741
wenzelm
parents: 65740
diff changeset
   329
      Timing(Time.ms(long(c1)), Time.ms(long(c2)), Time.ms(long(c3)))
wenzelm
parents: 65740
diff changeset
   330
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73367
diff changeset
   331
    def get[A](column: Column, f: Column => A): Option[A] = {
65740
83388f09e9ab clarified signature;
wenzelm
parents: 65739
diff changeset
   332
      val x = f(column)
77598
6370d9e5ab50 proper support for Option[Date] columns;
wenzelm
parents: 77596
diff changeset
   333
      if (rep.wasNull || x == null) None else Some(x)
65740
83388f09e9ab clarified signature;
wenzelm
parents: 65739
diff changeset
   334
    }
71601
97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA;
wenzelm
parents: 69980
diff changeset
   335
    def get_bool(column: Column): Option[Boolean] = get(column, bool)
97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA;
wenzelm
parents: 69980
diff changeset
   336
    def get_int(column: Column): Option[Int] = get(column, int)
97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA;
wenzelm
parents: 69980
diff changeset
   337
    def get_long(column: Column): Option[Long] = get(column, long)
97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA;
wenzelm
parents: 69980
diff changeset
   338
    def get_double(column: Column): Option[Double] = get(column, double)
97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA;
wenzelm
parents: 69980
diff changeset
   339
    def get_string(column: Column): Option[String] = get(column, string)
97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA;
wenzelm
parents: 69980
diff changeset
   340
    def get_bytes(column: Column): Option[Bytes] = get(column, bytes)
97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA;
wenzelm
parents: 69980
diff changeset
   341
    def get_date(column: Column): Option[Date] = get(column, date)
63790
3d723062dc70 more operations;
wenzelm
parents: 63788
diff changeset
   342
  }
65006
632bdf7b8bab clarified modules;
wenzelm
parents: 65004
diff changeset
   343
65740
83388f09e9ab clarified signature;
wenzelm
parents: 65739
diff changeset
   344
83388f09e9ab clarified signature;
wenzelm
parents: 65739
diff changeset
   345
  /* database */
83388f09e9ab clarified signature;
wenzelm
parents: 65739
diff changeset
   346
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73367
diff changeset
   347
  trait Database extends AutoCloseable {
65740
83388f09e9ab clarified signature;
wenzelm
parents: 65739
diff changeset
   348
    db =>
83388f09e9ab clarified signature;
wenzelm
parents: 65739
diff changeset
   349
77542
2da5562114c5 clarified signature: more uniform operations;
wenzelm
parents: 77541
diff changeset
   350
    def is_sqlite: Boolean = isInstanceOf[SQLite.Database]
2da5562114c5 clarified signature: more uniform operations;
wenzelm
parents: 77541
diff changeset
   351
    def is_postgresql: Boolean = isInstanceOf[PostgreSQL.Database]
76363
f7174238b5e3 no compression for database server: let PostgreSQL/TOAST do the job;
wenzelm
parents: 76122
diff changeset
   352
77348
885842575e2a more uniform operations;
wenzelm
parents: 77346
diff changeset
   353
    def rebuild(): Unit = ()
885842575e2a more uniform operations;
wenzelm
parents: 77346
diff changeset
   354
77527
790085b1002f more detailed table "isabelle_build_serial": allow to monitor activity of build_process instances;
wenzelm
parents: 77403
diff changeset
   355
    def now(): Date
790085b1002f more detailed table "isabelle_build_serial": allow to monitor activity of build_process instances;
wenzelm
parents: 77403
diff changeset
   356
65740
83388f09e9ab clarified signature;
wenzelm
parents: 65739
diff changeset
   357
65008
ed2eedf786f3 clarified handling of SQL.Type;
wenzelm
parents: 65007
diff changeset
   358
    /* types */
ed2eedf786f3 clarified handling of SQL.Type;
wenzelm
parents: 65007
diff changeset
   359
65730
7ae61e72a678 clarified signature;
wenzelm
parents: 65729
diff changeset
   360
    def sql_type(T: Type.Value): Source
65008
ed2eedf786f3 clarified handling of SQL.Type;
wenzelm
parents: 65007
diff changeset
   361
ed2eedf786f3 clarified handling of SQL.Type;
wenzelm
parents: 65007
diff changeset
   362
65006
632bdf7b8bab clarified modules;
wenzelm
parents: 65004
diff changeset
   363
    /* connection */
632bdf7b8bab clarified modules;
wenzelm
parents: 65004
diff changeset
   364
632bdf7b8bab clarified modules;
wenzelm
parents: 65004
diff changeset
   365
    def connection: Connection
632bdf7b8bab clarified modules;
wenzelm
parents: 65004
diff changeset
   366
77037
164a21e5d568 support specific connection types, for additional operations;
wenzelm
parents: 76870
diff changeset
   367
    def sqlite_connection: Option[JDBC4Connection] =
164a21e5d568 support specific connection types, for additional operations;
wenzelm
parents: 76870
diff changeset
   368
      connection match { case conn: JDBC4Connection => Some(conn) case _ => None }
164a21e5d568 support specific connection types, for additional operations;
wenzelm
parents: 76870
diff changeset
   369
164a21e5d568 support specific connection types, for additional operations;
wenzelm
parents: 76870
diff changeset
   370
    def postgresql_connection: Option[PGConnection] =
164a21e5d568 support specific connection types, for additional operations;
wenzelm
parents: 76870
diff changeset
   371
      connection match { case conn: PGConnection => Some(conn) case _ => None }
164a21e5d568 support specific connection types, for additional operations;
wenzelm
parents: 76870
diff changeset
   372
164a21e5d568 support specific connection types, for additional operations;
wenzelm
parents: 76870
diff changeset
   373
    def the_sqlite_connection: JDBC4Connection =
164a21e5d568 support specific connection types, for additional operations;
wenzelm
parents: 76870
diff changeset
   374
      sqlite_connection getOrElse
164a21e5d568 support specific connection types, for additional operations;
wenzelm
parents: 76870
diff changeset
   375
        error("SQLite connection expected, but found " + connection.getClass.getName)
164a21e5d568 support specific connection types, for additional operations;
wenzelm
parents: 76870
diff changeset
   376
164a21e5d568 support specific connection types, for additional operations;
wenzelm
parents: 76870
diff changeset
   377
    def the_postgresql_connection: PGConnection =
164a21e5d568 support specific connection types, for additional operations;
wenzelm
parents: 76870
diff changeset
   378
      postgresql_connection getOrElse
164a21e5d568 support specific connection types, for additional operations;
wenzelm
parents: 76870
diff changeset
   379
        error("PostgreSQL connection expected, but found " + connection.getClass.getName)
164a21e5d568 support specific connection types, for additional operations;
wenzelm
parents: 76870
diff changeset
   380
73367
77ef8bef0593 clarified signature --- fewer warnings;
wenzelm
parents: 73340
diff changeset
   381
    def close(): Unit = connection.close()
65006
632bdf7b8bab clarified modules;
wenzelm
parents: 65004
diff changeset
   382
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73367
diff changeset
   383
    def transaction[A](body: => A): A = {
75776
72e77c8307ec tuned signature, following hints by IntelliJ IDEA;
wenzelm
parents: 75393
diff changeset
   384
      val auto_commit = connection.getAutoCommit()
65006
632bdf7b8bab clarified modules;
wenzelm
parents: 65004
diff changeset
   385
      try {
632bdf7b8bab clarified modules;
wenzelm
parents: 65004
diff changeset
   386
        connection.setAutoCommit(false)
75776
72e77c8307ec tuned signature, following hints by IntelliJ IDEA;
wenzelm
parents: 75393
diff changeset
   387
        val savepoint = connection.setSavepoint()
65022
cda3d36aceb2 proper transaction for PostgreSQL;
wenzelm
parents: 65021
diff changeset
   388
        try {
cda3d36aceb2 proper transaction for PostgreSQL;
wenzelm
parents: 65021
diff changeset
   389
          val result = body
75776
72e77c8307ec tuned signature, following hints by IntelliJ IDEA;
wenzelm
parents: 75393
diff changeset
   390
          connection.commit()
65022
cda3d36aceb2 proper transaction for PostgreSQL;
wenzelm
parents: 65021
diff changeset
   391
          result
cda3d36aceb2 proper transaction for PostgreSQL;
wenzelm
parents: 65021
diff changeset
   392
        }
cda3d36aceb2 proper transaction for PostgreSQL;
wenzelm
parents: 65021
diff changeset
   393
        catch { case exn: Throwable => connection.rollback(savepoint); throw exn }
65006
632bdf7b8bab clarified modules;
wenzelm
parents: 65004
diff changeset
   394
      }
632bdf7b8bab clarified modules;
wenzelm
parents: 65004
diff changeset
   395
      finally { connection.setAutoCommit(auto_commit) }
632bdf7b8bab clarified modules;
wenzelm
parents: 65004
diff changeset
   396
    }
632bdf7b8bab clarified modules;
wenzelm
parents: 65004
diff changeset
   397
77596
dd8b08729458 clarified signature;
wenzelm
parents: 77591
diff changeset
   398
    def transaction_lock[A](tables: Tables)(body: => A): A =
dd8b08729458 clarified signature;
wenzelm
parents: 77591
diff changeset
   399
      transaction { tables.lock(db); body }
dd8b08729458 clarified signature;
wenzelm
parents: 77591
diff changeset
   400
dd8b08729458 clarified signature;
wenzelm
parents: 77591
diff changeset
   401
    def lock_tables(tables: List[Table]): Source = ""  // PostgreSQL only
77590
edc96be6b939 explicit locking for PostgreSQL --- neither available nor required for SQLite;
wenzelm
parents: 77552
diff changeset
   402
65006
632bdf7b8bab clarified modules;
wenzelm
parents: 65004
diff changeset
   403
65740
83388f09e9ab clarified signature;
wenzelm
parents: 65739
diff changeset
   404
    /* statements and results */
83388f09e9ab clarified signature;
wenzelm
parents: 65739
diff changeset
   405
83388f09e9ab clarified signature;
wenzelm
parents: 65739
diff changeset
   406
    def statement(sql: Source): Statement =
83388f09e9ab clarified signature;
wenzelm
parents: 65739
diff changeset
   407
      new Statement(db, connection.prepareStatement(sql))
65006
632bdf7b8bab clarified modules;
wenzelm
parents: 65004
diff changeset
   408
65740
83388f09e9ab clarified signature;
wenzelm
parents: 65739
diff changeset
   409
    def using_statement[A](sql: Source)(f: Statement => A): A =
83388f09e9ab clarified signature;
wenzelm
parents: 65739
diff changeset
   410
      using(statement(sql))(f)
65006
632bdf7b8bab clarified modules;
wenzelm
parents: 65004
diff changeset
   411
77541
9d9b30741fc4 tuned signature: reduce boilerplate;
wenzelm
parents: 77540
diff changeset
   412
    def execute_statement(sql: Source, body: Statement => Unit = _ => ()): Unit =
9d9b30741fc4 tuned signature: reduce boilerplate;
wenzelm
parents: 77540
diff changeset
   413
      using_statement(sql) { stmt => body(stmt); stmt.execute() }
77540
c537905c2125 tuned signature;
wenzelm
parents: 77537
diff changeset
   414
77552
080422b3d914 clarified signature: reduce boilerplate;
wenzelm
parents: 77543
diff changeset
   415
    def execute_query_statement[A, B](
080422b3d914 clarified signature: reduce boilerplate;
wenzelm
parents: 77543
diff changeset
   416
      sql: Source,
080422b3d914 clarified signature: reduce boilerplate;
wenzelm
parents: 77543
diff changeset
   417
      make_result: Iterator[A] => B,
080422b3d914 clarified signature: reduce boilerplate;
wenzelm
parents: 77543
diff changeset
   418
      get: Result => A
080422b3d914 clarified signature: reduce boilerplate;
wenzelm
parents: 77543
diff changeset
   419
    ): B = using_statement(sql)(stmt => make_result(stmt.execute_query().iterator(get)))
080422b3d914 clarified signature: reduce boilerplate;
wenzelm
parents: 77543
diff changeset
   420
080422b3d914 clarified signature: reduce boilerplate;
wenzelm
parents: 77543
diff changeset
   421
    def execute_query_statementO[A](sql: Source, get: Result => A): Option[A] =
080422b3d914 clarified signature: reduce boilerplate;
wenzelm
parents: 77543
diff changeset
   422
      execute_query_statement[A, Option[A]](sql, _.nextOption, get)
080422b3d914 clarified signature: reduce boilerplate;
wenzelm
parents: 77543
diff changeset
   423
080422b3d914 clarified signature: reduce boilerplate;
wenzelm
parents: 77543
diff changeset
   424
    def execute_query_statementB(sql: Source): Boolean =
080422b3d914 clarified signature: reduce boilerplate;
wenzelm
parents: 77543
diff changeset
   425
      using_statement(sql)(stmt => stmt.execute_query().next())
080422b3d914 clarified signature: reduce boilerplate;
wenzelm
parents: 77543
diff changeset
   426
65748
1f4a80e80c88 tuned signature;
wenzelm
parents: 65741
diff changeset
   427
    def update_date(stmt: Statement, i: Int, date: Date): Unit
65740
83388f09e9ab clarified signature;
wenzelm
parents: 65739
diff changeset
   428
    def date(res: Result, column: Column): Date
65006
632bdf7b8bab clarified modules;
wenzelm
parents: 65004
diff changeset
   429
65730
7ae61e72a678 clarified signature;
wenzelm
parents: 65729
diff changeset
   430
    def insert_permissive(table: Table, sql: Source = ""): Source
65703
cead65c19f2e more direct insert_permissive statement, which avoids somewhat fragile nested transactions;
wenzelm
parents: 65702
diff changeset
   431
65006
632bdf7b8bab clarified modules;
wenzelm
parents: 65004
diff changeset
   432
65669
d2f19b4a16ae support for views;
wenzelm
parents: 65668
diff changeset
   433
    /* tables and views */
65006
632bdf7b8bab clarified modules;
wenzelm
parents: 65004
diff changeset
   434
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73367
diff changeset
   435
    def tables: List[String] = {
65740
83388f09e9ab clarified signature;
wenzelm
parents: 65739
diff changeset
   436
      val result = new mutable.ListBuffer[String]
83388f09e9ab clarified signature;
wenzelm
parents: 65739
diff changeset
   437
      val rs = connection.getMetaData.getTables(null, null, "%", null)
83388f09e9ab clarified signature;
wenzelm
parents: 65739
diff changeset
   438
      while (rs.next) { result += rs.getString(3) }
83388f09e9ab clarified signature;
wenzelm
parents: 65739
diff changeset
   439
      result.toList
83388f09e9ab clarified signature;
wenzelm
parents: 65739
diff changeset
   440
    }
65006
632bdf7b8bab clarified modules;
wenzelm
parents: 65004
diff changeset
   441
65730
7ae61e72a678 clarified signature;
wenzelm
parents: 65729
diff changeset
   442
    def create_table(table: Table, strict: Boolean = false, sql: Source = ""): Unit =
77540
c537905c2125 tuned signature;
wenzelm
parents: 77537
diff changeset
   443
      execute_statement(table.create(strict, sql_type) + SQL.separate(sql))
65006
632bdf7b8bab clarified modules;
wenzelm
parents: 65004
diff changeset
   444
65018
8b36f225bbee clarified signature;
wenzelm
parents: 65014
diff changeset
   445
    def create_index(table: Table, name: String, columns: List[Column],
65280
ef37f5236794 prefer non-strict default;
wenzelm
parents: 65022
diff changeset
   446
        strict: Boolean = false, unique: Boolean = false): Unit =
77540
c537905c2125 tuned signature;
wenzelm
parents: 77537
diff changeset
   447
      execute_statement(table.create_index(name, columns, strict, unique))
65006
632bdf7b8bab clarified modules;
wenzelm
parents: 65004
diff changeset
   448
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73367
diff changeset
   449
    def create_view(table: Table, strict: Boolean = false): Unit = {
65691
2229276a1f99 eliminated redundant type SQL.View;
wenzelm
parents: 65690
diff changeset
   450
      if (strict || !tables.contains(table.name)) {
77540
c537905c2125 tuned signature;
wenzelm
parents: 77537
diff changeset
   451
        execute_statement("CREATE VIEW " + table + " AS " + { table.query; table.body })
65690
wenzelm
parents: 65677
diff changeset
   452
      }
65691
2229276a1f99 eliminated redundant type SQL.View;
wenzelm
parents: 65690
diff changeset
   453
    }
65006
632bdf7b8bab clarified modules;
wenzelm
parents: 65004
diff changeset
   454
  }
63778
e06e899b78d0 clarified modules;
wenzelm
parents:
diff changeset
   455
}
65006
632bdf7b8bab clarified modules;
wenzelm
parents: 65004
diff changeset
   456
632bdf7b8bab clarified modules;
wenzelm
parents: 65004
diff changeset
   457
632bdf7b8bab clarified modules;
wenzelm
parents: 65004
diff changeset
   458
632bdf7b8bab clarified modules;
wenzelm
parents: 65004
diff changeset
   459
/** SQLite **/
632bdf7b8bab clarified modules;
wenzelm
parents: 65004
diff changeset
   460
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73367
diff changeset
   461
object SQLite {
65021
da8ae577d171 clarified Date storage;
wenzelm
parents: 65020
diff changeset
   462
  // see https://www.sqlite.org/lang_datefunc.html
da8ae577d171 clarified Date storage;
wenzelm
parents: 65020
diff changeset
   463
  val date_format: Date.Format = Date.Format("uuuu-MM-dd HH:mm:ss.SSS x")
da8ae577d171 clarified Date storage;
wenzelm
parents: 65020
diff changeset
   464
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73367
diff changeset
   465
  lazy val init_jdbc: Unit = {
65890
1b004f5974af refer to already extracted library files, to avoid tmp files produced by SQLiteJDBCLoader, which tend to remain after JVM crash;
wenzelm
parents: 65804
diff changeset
   466
    val lib_path = Path.explode("$ISABELLE_SQLITE_HOME/" + Platform.jvm_platform)
76529
ded37aade88e clarified signature;
wenzelm
parents: 76363
diff changeset
   467
    val lib_name = File.get_file(lib_path).file_name
ded37aade88e clarified signature;
wenzelm
parents: 76363
diff changeset
   468
65890
1b004f5974af refer to already extracted library files, to avoid tmp files produced by SQLiteJDBCLoader, which tend to remain after JVM crash;
wenzelm
parents: 65804
diff changeset
   469
    System.setProperty("org.sqlite.lib.path", File.platform_path(lib_path))
1b004f5974af refer to already extracted library files, to avoid tmp files produced by SQLiteJDBCLoader, which tend to remain after JVM crash;
wenzelm
parents: 65804
diff changeset
   470
    System.setProperty("org.sqlite.lib.name", lib_name)
1b004f5974af refer to already extracted library files, to avoid tmp files produced by SQLiteJDBCLoader, which tend to remain after JVM crash;
wenzelm
parents: 65804
diff changeset
   471
1b004f5974af refer to already extracted library files, to avoid tmp files produced by SQLiteJDBCLoader, which tend to remain after JVM crash;
wenzelm
parents: 65804
diff changeset
   472
    Class.forName("org.sqlite.JDBC")
1b004f5974af refer to already extracted library files, to avoid tmp files produced by SQLiteJDBCLoader, which tend to remain after JVM crash;
wenzelm
parents: 65804
diff changeset
   473
  }
65292
e3bd1e7ddd23 more robust JDBC initialization, e.g. required for Isabelle/jEdit startup;
wenzelm
parents: 65280
diff changeset
   474
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73367
diff changeset
   475
  def open_database(path: Path): Database = {
65292
e3bd1e7ddd23 more robust JDBC initialization, e.g. required for Isabelle/jEdit startup;
wenzelm
parents: 65280
diff changeset
   476
    init_jdbc
65006
632bdf7b8bab clarified modules;
wenzelm
parents: 65004
diff changeset
   477
    val path0 = path.expand
632bdf7b8bab clarified modules;
wenzelm
parents: 65004
diff changeset
   478
    val s0 = File.platform_path(path0)
632bdf7b8bab clarified modules;
wenzelm
parents: 65004
diff changeset
   479
    val s1 = if (Platform.is_windows) s0.replace('\\', '/') else s0
632bdf7b8bab clarified modules;
wenzelm
parents: 65004
diff changeset
   480
    val connection = DriverManager.getConnection("jdbc:sqlite:" + s1)
65007
b6a1a1d42f5d clarified toString;
wenzelm
parents: 65006
diff changeset
   481
    new Database(path0.toString, connection)
65006
632bdf7b8bab clarified modules;
wenzelm
parents: 65004
diff changeset
   482
  }
632bdf7b8bab clarified modules;
wenzelm
parents: 65004
diff changeset
   483
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73367
diff changeset
   484
  class Database private[SQLite](name: String, val connection: Connection) extends SQL.Database {
65007
b6a1a1d42f5d clarified toString;
wenzelm
parents: 65006
diff changeset
   485
    override def toString: String = name
77540
c537905c2125 tuned signature;
wenzelm
parents: 77537
diff changeset
   486
    override def rebuild(): Unit = execute_statement("VACUUM")
65006
632bdf7b8bab clarified modules;
wenzelm
parents: 65004
diff changeset
   487
77527
790085b1002f more detailed table "isabelle_build_serial": allow to monitor activity of build_process instances;
wenzelm
parents: 77403
diff changeset
   488
    override def now(): Date = Date.now()
790085b1002f more detailed table "isabelle_build_serial": allow to monitor activity of build_process instances;
wenzelm
parents: 77403
diff changeset
   489
65730
7ae61e72a678 clarified signature;
wenzelm
parents: 65729
diff changeset
   490
    def sql_type(T: SQL.Type.Value): SQL.Source = SQL.sql_type_sqlite(T)
65011
42bffd1637f0 support for type Boolean;
wenzelm
parents: 65010
diff changeset
   491
65748
1f4a80e80c88 tuned signature;
wenzelm
parents: 65741
diff changeset
   492
    def update_date(stmt: SQL.Statement, i: Int, date: Date): Unit =
1f4a80e80c88 tuned signature;
wenzelm
parents: 65741
diff changeset
   493
      if (date == null) stmt.string(i) = (null: String)
1f4a80e80c88 tuned signature;
wenzelm
parents: 65741
diff changeset
   494
      else stmt.string(i) = date_format(date)
65598
5deef985e38e allow null;
wenzelm
parents: 65594
diff changeset
   495
65740
83388f09e9ab clarified signature;
wenzelm
parents: 65739
diff changeset
   496
    def date(res: SQL.Result, column: SQL.Column): Date =
77598
6370d9e5ab50 proper support for Option[Date] columns;
wenzelm
parents: 77596
diff changeset
   497
      proper_string(res.string(column)) match {
6370d9e5ab50 proper support for Option[Date] columns;
wenzelm
parents: 77596
diff changeset
   498
        case None => null
6370d9e5ab50 proper support for Option[Date] columns;
wenzelm
parents: 77596
diff changeset
   499
        case Some(s) => date_format.parse(s)
6370d9e5ab50 proper support for Option[Date] columns;
wenzelm
parents: 77596
diff changeset
   500
      }
65021
da8ae577d171 clarified Date storage;
wenzelm
parents: 65020
diff changeset
   501
65730
7ae61e72a678 clarified signature;
wenzelm
parents: 65729
diff changeset
   502
    def insert_permissive(table: SQL.Table, sql: SQL.Source = ""): SQL.Source =
77365
a10fa2112854 clarified signature;
wenzelm
parents: 77364
diff changeset
   503
      table.insert_cmd(cmd = "INSERT OR IGNORE", sql = sql)
65006
632bdf7b8bab clarified modules;
wenzelm
parents: 65004
diff changeset
   504
  }
632bdf7b8bab clarified modules;
wenzelm
parents: 65004
diff changeset
   505
}
632bdf7b8bab clarified modules;
wenzelm
parents: 65004
diff changeset
   506
632bdf7b8bab clarified modules;
wenzelm
parents: 65004
diff changeset
   507
632bdf7b8bab clarified modules;
wenzelm
parents: 65004
diff changeset
   508
632bdf7b8bab clarified modules;
wenzelm
parents: 65004
diff changeset
   509
/** PostgreSQL **/
632bdf7b8bab clarified modules;
wenzelm
parents: 65004
diff changeset
   510
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73367
diff changeset
   511
object PostgreSQL {
75967
ff164add75cd maintain "uuid" column in session build database, to identity the original build process uniquely;
wenzelm
parents: 75966
diff changeset
   512
  type Source = SQL.Source
ff164add75cd maintain "uuid" column in session build database, to identity the original build process uniquely;
wenzelm
parents: 75966
diff changeset
   513
65006
632bdf7b8bab clarified modules;
wenzelm
parents: 65004
diff changeset
   514
  val default_port = 5432
632bdf7b8bab clarified modules;
wenzelm
parents: 65004
diff changeset
   515
65292
e3bd1e7ddd23 more robust JDBC initialization, e.g. required for Isabelle/jEdit startup;
wenzelm
parents: 65280
diff changeset
   516
  lazy val init_jdbc: Unit = Class.forName("org.postgresql.Driver")
e3bd1e7ddd23 more robust JDBC initialization, e.g. required for Isabelle/jEdit startup;
wenzelm
parents: 65280
diff changeset
   517
65006
632bdf7b8bab clarified modules;
wenzelm
parents: 65004
diff changeset
   518
  def open_database(
632bdf7b8bab clarified modules;
wenzelm
parents: 65004
diff changeset
   519
    user: String,
632bdf7b8bab clarified modules;
wenzelm
parents: 65004
diff changeset
   520
    password: String,
632bdf7b8bab clarified modules;
wenzelm
parents: 65004
diff changeset
   521
    database: String = "",
632bdf7b8bab clarified modules;
wenzelm
parents: 65004
diff changeset
   522
    host: String = "",
65594
659305708959 clarified treatment of default port;
wenzelm
parents: 65593
diff changeset
   523
    port: Int = 0,
65636
df804cdba5f9 ssh_close for proper termination after use of database;
wenzelm
parents: 65620
diff changeset
   524
    ssh: Option[SSH.Session] = None,
77591
3f3dcf9f53f1 more robust transactions;
wenzelm
parents: 77590
diff changeset
   525
    ssh_close: Boolean = false,
3f3dcf9f53f1 more robust transactions;
wenzelm
parents: 77590
diff changeset
   526
    // see https://www.postgresql.org/docs/current/transaction-iso.html
3f3dcf9f53f1 more robust transactions;
wenzelm
parents: 77590
diff changeset
   527
    transaction_isolation: Int = Connection.TRANSACTION_SERIALIZABLE
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73367
diff changeset
   528
  ): Database = {
65292
e3bd1e7ddd23 more robust JDBC initialization, e.g. required for Isabelle/jEdit startup;
wenzelm
parents: 65280
diff changeset
   529
    init_jdbc
e3bd1e7ddd23 more robust JDBC initialization, e.g. required for Isabelle/jEdit startup;
wenzelm
parents: 65280
diff changeset
   530
65641
3b0110e25745 tuned message;
wenzelm
parents: 65636
diff changeset
   531
    if (user == "") error("Undefined database user")
65009
eda9366bbfac remote database access via ssh port forwarding;
wenzelm
parents: 65008
diff changeset
   532
65717
wenzelm
parents: 65706
diff changeset
   533
    val db_host = proper_string(host) getOrElse "localhost"
65594
659305708959 clarified treatment of default port;
wenzelm
parents: 65593
diff changeset
   534
    val db_port = if (port > 0 && port != default_port) ":" + port else ""
65717
wenzelm
parents: 65706
diff changeset
   535
    val db_name = "/" + (proper_string(database) getOrElse user)
65009
eda9366bbfac remote database access via ssh port forwarding;
wenzelm
parents: 65008
diff changeset
   536
65010
a27e9908dcf7 clarified signature;
wenzelm
parents: 65009
diff changeset
   537
    val (url, name, port_forwarding) =
65009
eda9366bbfac remote database access via ssh port forwarding;
wenzelm
parents: 65008
diff changeset
   538
      ssh match {
65010
a27e9908dcf7 clarified signature;
wenzelm
parents: 65009
diff changeset
   539
        case None =>
a27e9908dcf7 clarified signature;
wenzelm
parents: 65009
diff changeset
   540
          val spec = db_host + db_port + db_name
a27e9908dcf7 clarified signature;
wenzelm
parents: 65009
diff changeset
   541
          val url = "jdbc:postgresql://" + spec
a27e9908dcf7 clarified signature;
wenzelm
parents: 65009
diff changeset
   542
          val name = user + "@" + spec
a27e9908dcf7 clarified signature;
wenzelm
parents: 65009
diff changeset
   543
          (url, name, None)
65009
eda9366bbfac remote database access via ssh port forwarding;
wenzelm
parents: 65008
diff changeset
   544
        case Some(ssh) =>
65594
659305708959 clarified treatment of default port;
wenzelm
parents: 65593
diff changeset
   545
          val fw =
659305708959 clarified treatment of default port;
wenzelm
parents: 65593
diff changeset
   546
            ssh.port_forwarding(remote_host = db_host,
65636
df804cdba5f9 ssh_close for proper termination after use of database;
wenzelm
parents: 65620
diff changeset
   547
              remote_port = if (port > 0) port else default_port,
df804cdba5f9 ssh_close for proper termination after use of database;
wenzelm
parents: 65620
diff changeset
   548
              ssh_close = ssh_close)
76122
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 75967
diff changeset
   549
          val url = "jdbc:postgresql://localhost:" + fw.port + db_name
65010
a27e9908dcf7 clarified signature;
wenzelm
parents: 65009
diff changeset
   550
          val name = user + "@" + fw + db_name + " via ssh " + ssh
a27e9908dcf7 clarified signature;
wenzelm
parents: 65009
diff changeset
   551
          (url, name, Some(fw))
65009
eda9366bbfac remote database access via ssh port forwarding;
wenzelm
parents: 65008
diff changeset
   552
      }
eda9366bbfac remote database access via ssh port forwarding;
wenzelm
parents: 65008
diff changeset
   553
    try {
65010
a27e9908dcf7 clarified signature;
wenzelm
parents: 65009
diff changeset
   554
      val connection = DriverManager.getConnection(url, user, password)
77591
3f3dcf9f53f1 more robust transactions;
wenzelm
parents: 77590
diff changeset
   555
      connection.setTransactionIsolation(transaction_isolation)
65010
a27e9908dcf7 clarified signature;
wenzelm
parents: 65009
diff changeset
   556
      new Database(name, connection, port_forwarding)
65009
eda9366bbfac remote database access via ssh port forwarding;
wenzelm
parents: 65008
diff changeset
   557
    }
73367
77ef8bef0593 clarified signature --- fewer warnings;
wenzelm
parents: 73340
diff changeset
   558
    catch { case exn: Throwable => port_forwarding.foreach(_.close()); throw exn }
65006
632bdf7b8bab clarified modules;
wenzelm
parents: 65004
diff changeset
   559
  }
632bdf7b8bab clarified modules;
wenzelm
parents: 65004
diff changeset
   560
65009
eda9366bbfac remote database access via ssh port forwarding;
wenzelm
parents: 65008
diff changeset
   561
  class Database private[PostgreSQL](
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73367
diff changeset
   562
    name: String,
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73367
diff changeset
   563
    val connection: Connection,
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73367
diff changeset
   564
    port_forwarding: Option[SSH.Port_Forwarding]
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73367
diff changeset
   565
  ) extends SQL.Database {
65010
a27e9908dcf7 clarified signature;
wenzelm
parents: 65009
diff changeset
   566
    override def toString: String = name
65008
ed2eedf786f3 clarified handling of SQL.Type;
wenzelm
parents: 65007
diff changeset
   567
77527
790085b1002f more detailed table "isabelle_build_serial": allow to monitor activity of build_process instances;
wenzelm
parents: 77403
diff changeset
   568
    override def now(): Date = {
790085b1002f more detailed table "isabelle_build_serial": allow to monitor activity of build_process instances;
wenzelm
parents: 77403
diff changeset
   569
      val now = SQL.Column.date("now")
77552
080422b3d914 clarified signature: reduce boilerplate;
wenzelm
parents: 77543
diff changeset
   570
      execute_query_statementO[Date]("SELECT NOW() as " + now.ident, res => res.date(now))
080422b3d914 clarified signature: reduce boilerplate;
wenzelm
parents: 77543
diff changeset
   571
        .getOrElse(error("Failed to get current date/time from database server " + toString))
77527
790085b1002f more detailed table "isabelle_build_serial": allow to monitor activity of build_process instances;
wenzelm
parents: 77403
diff changeset
   572
    }
790085b1002f more detailed table "isabelle_build_serial": allow to monitor activity of build_process instances;
wenzelm
parents: 77403
diff changeset
   573
65730
7ae61e72a678 clarified signature;
wenzelm
parents: 65729
diff changeset
   574
    def sql_type(T: SQL.Type.Value): SQL.Source = SQL.sql_type_postgresql(T)
65009
eda9366bbfac remote database access via ssh port forwarding;
wenzelm
parents: 65008
diff changeset
   575
65021
da8ae577d171 clarified Date storage;
wenzelm
parents: 65020
diff changeset
   576
    // see https://jdbc.postgresql.org/documentation/head/8-date-time.html
65748
1f4a80e80c88 tuned signature;
wenzelm
parents: 65741
diff changeset
   577
    def update_date(stmt: SQL.Statement, i: Int, date: Date): Unit =
65740
83388f09e9ab clarified signature;
wenzelm
parents: 65739
diff changeset
   578
      if (date == null) stmt.rep.setObject(i, null)
69980
f2e3adfd916f tuned signature;
wenzelm
parents: 69393
diff changeset
   579
      else stmt.rep.setObject(i, OffsetDateTime.from(date.to(Date.timezone_utc).rep))
65598
5deef985e38e allow null;
wenzelm
parents: 65594
diff changeset
   580
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73367
diff changeset
   581
    def date(res: SQL.Result, column: SQL.Column): Date = {
65740
83388f09e9ab clarified signature;
wenzelm
parents: 65739
diff changeset
   582
      val obj = res.rep.getObject(column.name, classOf[OffsetDateTime])
65704
aa9a7a753296 more robust;
wenzelm
parents: 65703
diff changeset
   583
      if (obj == null) null else Date.instant(obj.toInstant)
aa9a7a753296 more robust;
wenzelm
parents: 65703
diff changeset
   584
    }
65021
da8ae577d171 clarified Date storage;
wenzelm
parents: 65020
diff changeset
   585
65730
7ae61e72a678 clarified signature;
wenzelm
parents: 65729
diff changeset
   586
    def insert_permissive(table: SQL.Table, sql: SQL.Source = ""): SQL.Source =
77377
82fdc7cf9d44 tuned whitespace in generated SQL;
wenzelm
parents: 77375
diff changeset
   587
      table.insert_cmd(sql = if_proper(sql, sql + " ") + "ON CONFLICT DO NOTHING")
65703
cead65c19f2e more direct insert_permissive statement, which avoids somewhat fragile nested transactions;
wenzelm
parents: 65702
diff changeset
   588
77039
2f09dc0e6dda support IPC via database server;
wenzelm
parents: 77037
diff changeset
   589
77590
edc96be6b939 explicit locking for PostgreSQL --- neither available nor required for SQLite;
wenzelm
parents: 77552
diff changeset
   590
    /* explicit locking: only applicable to PostgreSQL within transaction context */
edc96be6b939 explicit locking for PostgreSQL --- neither available nor required for SQLite;
wenzelm
parents: 77552
diff changeset
   591
    // see https://www.postgresql.org/docs/current/sql-lock.html
edc96be6b939 explicit locking for PostgreSQL --- neither available nor required for SQLite;
wenzelm
parents: 77552
diff changeset
   592
    // see https://www.postgresql.org/docs/current/explicit-locking.html
edc96be6b939 explicit locking for PostgreSQL --- neither available nor required for SQLite;
wenzelm
parents: 77552
diff changeset
   593
77596
dd8b08729458 clarified signature;
wenzelm
parents: 77591
diff changeset
   594
    override def lock_tables(tables: List[SQL.Table]): PostgreSQL.Source =
dd8b08729458 clarified signature;
wenzelm
parents: 77591
diff changeset
   595
      "LOCK TABLE " + tables.mkString(", ") + " IN ACCESS EXCLUSIVE MODE"
77590
edc96be6b939 explicit locking for PostgreSQL --- neither available nor required for SQLite;
wenzelm
parents: 77552
diff changeset
   596
edc96be6b939 explicit locking for PostgreSQL --- neither available nor required for SQLite;
wenzelm
parents: 77552
diff changeset
   597
77039
2f09dc0e6dda support IPC via database server;
wenzelm
parents: 77037
diff changeset
   598
    /* notifications: IPC via database server */
2f09dc0e6dda support IPC via database server;
wenzelm
parents: 77037
diff changeset
   599
    // see https://www.postgresql.org/docs/current/sql-notify.html
2f09dc0e6dda support IPC via database server;
wenzelm
parents: 77037
diff changeset
   600
2f09dc0e6dda support IPC via database server;
wenzelm
parents: 77037
diff changeset
   601
    def listen(name: String): Unit =
77541
9d9b30741fc4 tuned signature: reduce boilerplate;
wenzelm
parents: 77540
diff changeset
   602
      execute_statement("LISTEN " + SQL.ident(name))
77039
2f09dc0e6dda support IPC via database server;
wenzelm
parents: 77037
diff changeset
   603
2f09dc0e6dda support IPC via database server;
wenzelm
parents: 77037
diff changeset
   604
    def unlisten(name: String = "*"): Unit =
77541
9d9b30741fc4 tuned signature: reduce boilerplate;
wenzelm
parents: 77540
diff changeset
   605
      execute_statement("UNLISTEN " + (if (name == "*") name else SQL.ident(name)))
77039
2f09dc0e6dda support IPC via database server;
wenzelm
parents: 77037
diff changeset
   606
2f09dc0e6dda support IPC via database server;
wenzelm
parents: 77037
diff changeset
   607
    def notify(name: String, payload: String = ""): Unit =
77543
97b5547f2b17 tuned whitespace and braces;
wenzelm
parents: 77542
diff changeset
   608
      execute_statement("NOTIFY " + SQL.ident(name) + if_proper(payload, ", " + SQL.string(payload)))
77039
2f09dc0e6dda support IPC via database server;
wenzelm
parents: 77037
diff changeset
   609
2f09dc0e6dda support IPC via database server;
wenzelm
parents: 77037
diff changeset
   610
    def get_notifications(): List[PGNotification] =
2f09dc0e6dda support IPC via database server;
wenzelm
parents: 77037
diff changeset
   611
      the_postgresql_connection.getNotifications() match {
2f09dc0e6dda support IPC via database server;
wenzelm
parents: 77037
diff changeset
   612
        case null => Nil
2f09dc0e6dda support IPC via database server;
wenzelm
parents: 77037
diff changeset
   613
        case array => array.toList
2f09dc0e6dda support IPC via database server;
wenzelm
parents: 77037
diff changeset
   614
      }
2f09dc0e6dda support IPC via database server;
wenzelm
parents: 77037
diff changeset
   615
2f09dc0e6dda support IPC via database server;
wenzelm
parents: 77037
diff changeset
   616
73367
77ef8bef0593 clarified signature --- fewer warnings;
wenzelm
parents: 73340
diff changeset
   617
    override def close(): Unit = { super.close(); port_forwarding.foreach(_.close()) }
65006
632bdf7b8bab clarified modules;
wenzelm
parents: 65004
diff changeset
   618
  }
632bdf7b8bab clarified modules;
wenzelm
parents: 65004
diff changeset
   619
}