--- a/Admin/components/components.sha1 Wed Apr 24 20:41:35 2024 +0200
+++ b/Admin/components/components.sha1 Fri Apr 26 19:15:37 2024 +0200
@@ -240,6 +240,7 @@
258d527819583d740a3aa52dfef630eed389f8c6 jedit-20211019.tar.gz
f4f3fcbd54488297a5d2fcd23a2595912d5ba80b jedit-20211103.tar.gz
7fc9df033ec6b49dc1dad85eb240ab4f80653aa3 jedit-20231120.tar.gz
+fbfd1d8a117a5bd844f230903d561cb88d3e5189 jedit-20240425.tar.gz
44775a22f42a9d665696bfb49e53c79371c394b0 jedit_build-20111217.tar.gz
a242a688810f2bccf24587b0062ce8027bf77fa2 jedit_build-20120304.tar.gz
4c948dee53f74361c097c08f49a1a5ff9b17bd1d jedit_build-20120307.tar.gz
--- a/Admin/components/main Wed Apr 24 20:41:35 2024 +0200
+++ b/Admin/components/main Fri Apr 26 19:15:37 2024 +0200
@@ -14,7 +14,7 @@
isabelle_setup-20240327
javamail-20240109
jdk-21.0.3
-jedit-20231120
+jedit-20240425
jfreechart-1.5.3
jortho-1.0-2
jsoup-1.17.2
--- a/src/Tools/jEdit/patches/extended_styles_brackets Wed Apr 24 20:41:35 2024 +0200
+++ b/src/Tools/jEdit/patches/extended_styles_brackets Fri Apr 26 19:15:37 2024 +0200
@@ -1,6 +1,6 @@
diff -ru jedit5.6.0/jEdit/org/gjt/sp/jedit/syntax/Chunk.java jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/syntax/Chunk.java
--- jedit5.6.0/jEdit/org/gjt/sp/jedit/syntax/Chunk.java 2020-09-03 05:31:01.000000000 +0200
-+++ jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/syntax/Chunk.java 2021-05-10 11:02:05.816257745 +0200
++++ jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/syntax/Chunk.java 2024-04-25 12:56:22.208257322 +0200
@@ -332,9 +332,9 @@
//{{{ Package private members
@@ -24,6 +24,18 @@
private GlyphData glyphData;
//}}}
+@@ -926,6 +926,11 @@
+ }
+
+ @Override
++ public GlyphData computeIfAbsent(GlyphKey key, java.util.function.Function<? super GlyphKey, ? extends GlyphData> f) {
++ synchronized (this) { return super.computeIfAbsent(key, f); }
++ }
++
++ @Override
+ protected boolean removeEldestEntry(Map.Entry<GlyphKey, GlyphData> eldest)
+ {
+ return size() > capacity;
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 2023-11-20 15:31:55.825519645 +0100