src/Pure/General/sql.scala

 /*  Title:      Pure/General/sql.scala
     Author:     Makarius
 
 Support for SQL databases: SQLite and PostgreSQL.
 
-See https://docs.oracle.com/en/java/javase/17/docs/api/java.sql/java/sql/Connection.html
+See https://docs.oracle.com/en/java/javase/21/docs/api/java.sql/java/sql/Connection.html
 */
 
 package isabelle
 
 

 
 
 
 /** PostgreSQL **/
 
-// see https://www.postgresql.org/docs/current/index.html
+// see https://www.postgresql.org/docs/14/index.html
 // see https://jdbc.postgresql.org/documentation
 
 object PostgreSQL {
   type Source = SQL.Source
 

     def insert_permissive(table: SQL.Table, sql: SQL.Source = ""): SQL.Source =
       table.insert_cmd(sql = if_proper(sql, sql + " ") + "ON CONFLICT DO NOTHING")
 
 
     /* explicit locking: only applicable to PostgreSQL within transaction context */
-    // see https://www.postgresql.org/docs/current/sql-lock.html
-    // see https://www.postgresql.org/docs/current/explicit-locking.html
+    // see https://www.postgresql.org/docs/14/sql-lock.html
+    // see https://www.postgresql.org/docs/14/explicit-locking.html
 
     override def lock_tables(tables: List[SQL.Table]): PostgreSQL.Source =
       if_proper(tables, "LOCK TABLE " + tables.mkString(", ") + " IN ACCESS EXCLUSIVE MODE")
 
 
     /* notifications: IPC via database server */
     /*
-      - see https://www.postgresql.org/docs/current/sql-notify.html
+      - see https://www.postgresql.org/docs/14/sql-notify.html
       - self-notifications and repeated notifications are suppressed
       - notifications are sorted by local system time (nano seconds)
     */
 
     private var _receiver_buffer: Option[Map[SQL.Notification, Long]] = None