--- a/src/Doc/JEdit/JEdit.thy Wed Nov 04 18:32:47 2015 +0100
+++ b/src/Doc/JEdit/JEdit.thy Wed Nov 04 18:35:50 2015 +0100
@@ -976,7 +976,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
- "http://docs.oracle.com/javase/7/docs/api/java/util/regex/Pattern.html"}\<close>
+ "https://docs.oracle.com/javase/8/docs/api/java/util/regex/Pattern.html"}\<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.