# HG changeset patch
# User wenzelm
# Date 1700492110 -3600
# Node ID b6bca0666c38334c06dd7fc98f93c4e51f383de5
# Parent  d9b32243798f58ec7d58aadf65ebd87727086f20
rebuild jedit with minimal patch for jdk-21, following SVN 25690;

diff -r d9b32243798f -r b6bca0666c38 Admin/components/components.sha1
--- a/Admin/components/components.sha1	Mon Nov 20 14:23:11 2023 +0100
+++ b/Admin/components/components.sha1	Mon Nov 20 15:55:10 2023 +0100
@@ -228,6 +228,7 @@
 0e4fd4d66388ddc760fa5fbd8d4a9a3b77cf59c7 jedit-20210802.tar.gz
 258d527819583d740a3aa52dfef630eed389f8c6 jedit-20211019.tar.gz
 f4f3fcbd54488297a5d2fcd23a2595912d5ba80b jedit-20211103.tar.gz
+7fc9df033ec6b49dc1dad85eb240ab4f80653aa3 jedit-20231120.tar.gz
 44775a22f42a9d665696bfb49e53c79371c394b0 jedit_build-20111217.tar.gz
 a242a688810f2bccf24587b0062ce8027bf77fa2 jedit_build-20120304.tar.gz
 4c948dee53f74361c097c08f49a1a5ff9b17bd1d jedit_build-20120307.tar.gz
diff -r d9b32243798f -r b6bca0666c38 Admin/components/main
--- a/Admin/components/main	Mon Nov 20 14:23:11 2023 +0100
+++ b/Admin/components/main	Mon Nov 20 15:55:10 2023 +0100
@@ -14,7 +14,7 @@
 isabelle_setup-20230922
 javamail-1.4.7
 jdk-17.0.7
-jedit-20211103
+jedit-20231120
 jfreechart-1.5.3
 jortho-1.0-2
 jsoup-1.15.4
diff -r d9b32243798f -r b6bca0666c38 src/Tools/jEdit/patches/extended_styles_brackets
--- a/src/Tools/jEdit/patches/extended_styles_brackets	Mon Nov 20 14:23:11 2023 +0100
+++ b/src/Tools/jEdit/patches/extended_styles_brackets	Mon Nov 20 15:55:10 2023 +0100
@@ -26,7 +26,7 @@
  
 diff -ru jedit5.6.0/jEdit/org/gjt/sp/jedit/textarea/TextArea.java jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/textarea/TextArea.java
 --- jedit5.6.0/jEdit/org/gjt/sp/jedit/textarea/TextArea.java	2020-09-03 05:31:01.000000000 +0200
-+++ jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/textarea/TextArea.java	2021-05-10 18:19:56.275495525 +0200
++++ jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/textarea/TextArea.java	2023-11-20 15:31:55.825519645 +0100
 @@ -914,6 +914,11 @@
  		return chunkCache.getLineInfo(screenLine).physicalLine;
  	} //}}}
@@ -50,6 +50,15 @@
  		int count = 1;
  		char openBracket = '\0';
  		char closeBracket = '\0';
+@@ -6336,7 +6341,7 @@
+ 		{
+ 			int following = charBreaker.following(offset -
+ 					index0Offset);
+-			if (following == BreakIterator.DONE)
++			if (following == BreakIterator.DONE || (Runtime.version().feature() >= 20 && following == offset - index0Offset))
+ 			{
+ 				// This means a end of line. Then it is
+ 				// safe to assume 1 code unit is a character.
 diff -ru jedit5.6.0/jEdit/org/gjt/sp/jedit/TextUtilities.java jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/TextUtilities.java
 --- jedit5.6.0/jEdit/org/gjt/sp/jedit/TextUtilities.java	2020-09-03 05:31:03.000000000 +0200
 +++ jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/TextUtilities.java	2021-05-10 18:20:57.418571547 +0200