# HG changeset patch
# User wenzelm
# Date 1583523196 -3600
# Node ID e977609c30eb6502c1422895281d6dbb70cc29b8
# Parent  62755ec99671fef36f54b9a8d888f638a30e8818
formally depend on Java 11 --- discontinue Java 8 workaround;

diff -r 62755ec99671 -r e977609c30eb src/Doc/JEdit/JEdit.thy
--- a/src/Doc/JEdit/JEdit.thy	Fri Mar 06 20:18:21 2020 +0100
+++ b/src/Doc/JEdit/JEdit.thy	Fri Mar 06 20:33:16 2020 +0100
@@ -2165,18 +2165,6 @@
 chapter \<open>Known problems and workarounds \label{sec:problems}\<close>
 
 text \<open>
-  \<^item> \<^bold>\<open>Problem:\<close> Font-rendering in Java 11 (OpenJDK) is worse than Java 8
-  (by Oracle) on low-quality displays.
-
-  \<^bold>\<open>Workaround:\<close> Find an old copy of Java 8 from Oracle (which has
-  ``end-of-life'' status since Jan-2019) and refer to its main directory via
-  @{setting "ISABELLE_JDK_HOME"}\<^verbatim>\<open>="..."\<close> in
-  \<^path>\<open>$ISABELLE_HOME_USER/etc/settings\<close>. Also add
-  \<^verbatim>\<open>isabelle_fonts_hinted=false\<close> to
-  \<^path>\<open>$ISABELLE_HOME_USER/etc/preferences\<close> to avoid problems of the old
-  font renderer with hinting. Run the application from the command-line as
-  @{tool jedit}.
-
   \<^item> \<^bold>\<open>Problem:\<close> Keyboard shortcuts \<^verbatim>\<open>C+PLUS\<close> and \<^verbatim>\<open>C+MINUS\<close> for adjusting the
   editor font size depend on platform details and national keyboards.
 
diff -r 62755ec99671 -r e977609c30eb src/Doc/System/Server.thy
--- a/src/Doc/System/Server.thy	Fri Mar 06 20:18:21 2020 +0100
+++ b/src/Doc/System/Server.thy	Fri Mar 06 20:33:16 2020 +0100
@@ -493,7 +493,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/javase/8/docs/api/java/util/UUID.html\<close>.\<close> Such
+  \<^url>\<open>https://docs.oracle.com/en/java/javase/11/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 62755ec99671 -r e977609c30eb src/Tools/jEdit/src-base/Isabelle_Base.props
--- a/src/Tools/jEdit/src-base/Isabelle_Base.props	Fri Mar 06 20:18:21 2020 +0100
+++ b/src/Tools/jEdit/src-base/Isabelle_Base.props	Fri Mar 06 20:33:16 2020 +0100
@@ -13,5 +13,5 @@
 plugin.isabelle.jedit_base.Plugin.usePluginHome=false
 
 #dependencies
-plugin.isabelle.jedit_base.Plugin.depend.0=jdk 1.8
+plugin.isabelle.jedit_base.Plugin.depend.0=jdk 11
 plugin.isabelle.jedit_base.Plugin.depend.1=jedit 05.05.00.00
diff -r 62755ec99671 -r e977609c30eb src/Tools/jEdit/src/Isabelle.props
--- a/src/Tools/jEdit/src/Isabelle.props	Fri Mar 06 20:18:21 2020 +0100
+++ b/src/Tools/jEdit/src/Isabelle.props	Fri Mar 06 20:33:16 2020 +0100
@@ -13,7 +13,7 @@
 plugin.isabelle.jedit.Plugin.usePluginHome=false
 
 #dependencies
-plugin.isabelle.jedit.Plugin.depend.0=jdk 1.8
+plugin.isabelle.jedit.Plugin.depend.0=jdk 11
 plugin.isabelle.jedit.Plugin.depend.1=jedit 05.05.00.00
 plugin.isabelle.jedit.Plugin.depend.2=plugin console.ConsolePlugin 5.1.4
 plugin.isabelle.jedit.Plugin.depend.3=plugin errorlist.ErrorListPlugin 2.3