# HG changeset patch
# User wenzelm
# Date 1708811816 -3600
# Node ID 54d0f6edfe3a00679bc1d1069f0cb7129c86111a
# Parent  aa77ebb2dc16ce4297d4384d7d2bb31ae47fe759
clarified versions for documentation;

diff -r aa77ebb2dc16 -r 54d0f6edfe3a src/Doc/JEdit/JEdit.thy
--- a/src/Doc/JEdit/JEdit.thy	Sat Feb 24 22:15:42 2024 +0100
+++ b/src/Doc/JEdit/JEdit.thy	Sat Feb 24 22:56:56 2024 +0100
@@ -1153,7 +1153,7 @@
 
     \<^item> The \<^emph>\<open>Search\<close> field allows to highlight query output according to some
     regular expression, in the notation that is commonly used on the Java
-    platform.\<^footnote>\<open>\<^url>\<open>https://docs.oracle.com/en/java/javase/17/docs/api/java.base/java/util/regex/Pattern.html\<close>\<close>
+    platform.\<^footnote>\<open>\<^url>\<open>https://docs.oracle.com/en/java/javase/21/docs/api/java.base/java/util/regex/Pattern.html\<close>\<close>
     This may serve as an additional visual filter of the result.
 
     \<^item> The \<^emph>\<open>Zoom\<close> box controls the font size of the output area.
diff -r aa77ebb2dc16 -r 54d0f6edfe3a src/Doc/System/Scala.thy
--- a/src/Doc/System/Scala.thy	Sat Feb 24 22:15:42 2024 +0100
+++ b/src/Doc/System/Scala.thy	Sat Feb 24 22:56:56 2024 +0100
@@ -132,7 +132,7 @@
 
   \<^medskip>
   The syntax of \<^path>\<open>etc/build.props\<close> follows a regular Java properties
-  file\<^footnote>\<open>\<^url>\<open>https://docs.oracle.com/en/java/javase/17/docs/api/java.base/java/util/Properties.html#load(java.io.Reader)\<close>\<close>,
+  file\<^footnote>\<open>\<^url>\<open>https://docs.oracle.com/en/java/javase/21/docs/api/java.base/java/util/Properties.html#load(java.io.Reader)\<close>\<close>,
   but the encoding is \<^verbatim>\<open>UTF-8\<close>, instead of historic \<^verbatim>\<open>ISO 8859-1\<close> from the API
   documentation.
 
diff -r aa77ebb2dc16 -r 54d0f6edfe3a src/Doc/System/Server.thy
--- a/src/Doc/System/Server.thy	Sat Feb 24 22:15:42 2024 +0100
+++ b/src/Doc/System/Server.thy	Sat Feb 24 22:56:56 2024 +0100
@@ -491,7 +491,7 @@
 
   \<^item> \<^bold>\<open>type\<close>~\<open>uuid = string\<close> refers to a Universally Unique Identifier (UUID)
   as plain text.\<^footnote>\<open>See \<^url>\<open>https://www.ietf.org/rfc/rfc4122.txt\<close> and
-  \<^url>\<open>https://docs.oracle.com/en/java/javase/17/docs/api/java.base/java/util/UUID.html\<close>.\<close> Such
+  \<^url>\<open>https://docs.oracle.com/en/java/javase/21/docs/api/java.base/java/util/UUID.html\<close>.\<close> Such
   identifiers are created as private random numbers of the server and only
   revealed to the client that creates a certain resource (e.g.\ task or
   session). A client may disclose this information for use in a different
diff -r aa77ebb2dc16 -r 54d0f6edfe3a src/Doc/System/Sessions.thy
--- a/src/Doc/System/Sessions.thy	Sat Feb 24 22:15:42 2024 +0100
+++ b/src/Doc/System/Sessions.thy	Sat Feb 24 22:56:56 2024 +0100
@@ -662,7 +662,7 @@
   turned into plain spaces (according to their formal width).
 
   The syntax for patters follows regular expressions of the Java
-  platform.\<^footnote>\<open>\<^url>\<open>https://docs.oracle.com/en/java/javase/17/docs/api/java.base/java/util/regex/Pattern.html\<close>\<close>
+  platform.\<^footnote>\<open>\<^url>\<open>https://docs.oracle.com/en/java/javase/21/docs/api/java.base/java/util/regex/Pattern.html\<close>\<close>
 \<close>
 
 subsubsection \<open>Examples\<close>
diff -r aa77ebb2dc16 -r 54d0f6edfe3a src/Pure/General/sql.scala
--- a/src/Pure/General/sql.scala	Sat Feb 24 22:15:42 2024 +0100
+++ b/src/Pure/General/sql.scala	Sat Feb 24 22:56:56 2024 +0100
@@ -3,7 +3,7 @@
 
 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
@@ -662,7 +662,7 @@
 
 /** 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 {
@@ -778,8 +778,8 @@
 
 
     /* 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")
@@ -787,7 +787,7 @@
 
     /* 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)
     */