--- 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.
--- 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.
--- 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
--- 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>
--- 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)
*/