# HG changeset patch
# User wenzelm
# Date 1741774928 -3600
# Node ID 756e88885a7c5f476dee3467be97fc58f4aaef13
# Parent  b6eb006562747d13de0dc4651e5623e6fa4f8b8d
tuned;

diff -r b6eb00656274 -r 756e88885a7c src/Doc/JEdit/JEdit.thy
--- a/src/Doc/JEdit/JEdit.thy	Wed Mar 12 11:11:45 2025 +0100
+++ b/src/Doc/JEdit/JEdit.thy	Wed Mar 12 11:22:08 2025 +0100
@@ -336,7 +336,7 @@
   technical problems have accumulated in recent years (e.g.\ see
   \secref{sec:problems}).
 
-  In 2021, we are de-facto back to \<^emph>\<open>portable look-and-feels\<close>, which also
+  Since 2021, we are de-facto back to \<^emph>\<open>portable look-and-feels\<close>, which also
   happen to be \emph{scalable} on high-resolution displays:
 
     \<^item> \<^verbatim>\<open>FlatLaf Light\<close> is the default for Isabelle/jEdit on all platforms. It
@@ -1040,9 +1040,8 @@
 
   \<^medskip>
   \<^emph>\<open>Explicit highlighting\<close> of output works via the \<^emph>\<open>Search\<close> field: it matches
-  the text agains a given regular expression, in the notation that is commonly
-  used on the Java
-  platform.\<^footnote>\<open>\<^url>\<open>https://docs.oracle.com/en/java/javase/21/docs/api/java.base/java/util/regex/Pattern.html\<close>\<close>
+  the text against a given regular expression, in the notation of
+  Java.\<^footnote>\<open>\<^url>\<open>https://docs.oracle.com/en/java/javase/21/docs/api/java.base/java/util/regex/Pattern.html\<close>\<close>
   Results are also presented as a tree view, by sub-dividing the output panel
   on demand.