update to jedit-20250822, with support for EditPaneFactory and JEditTextAreaFactory as services;
--- a/Admin/components/components.sha1 Fri Aug 22 13:30:21 2025 +0200
+++ b/Admin/components/components.sha1 Fri Aug 22 15:53:50 2025 +0200
@@ -282,6 +282,7 @@
62cce488b1c5541de7a56a4a49537037da2bfd44 jedit-20250516.tar.gz
5789aa61bb37a8003a2b6e1037d217057e51cdc9 jedit-20250520.tar.gz
a141f565676050b8b6e6e97629778f96a81d9706 jedit-20250521.tar.gz
+a7c57e9e3aba1b6d18210818816b2fc9a555df68 jedit-20250822.tar.gz
44775a22f42a9d665696bfb49e53c79371c394b0 jedit_build-20111217.tar.gz
a242a688810f2bccf24587b0062ce8027bf77fa2 jedit_build-20120304.tar.gz
4c948dee53f74361c097c08f49a1a5ff9b17bd1d jedit_build-20120307.tar.gz
--- a/Admin/components/main Fri Aug 22 13:30:21 2025 +0200
+++ b/Admin/components/main Fri Aug 22 15:53:50 2025 +0200
@@ -15,7 +15,7 @@
isabelle_setup-20250613
javamail-20250122
jdk-21.0.8
-jedit-20250521
+jedit-20250822
jfreechart-1.5.3
jortho-1.0-2
jsoup-1.18.3
--- a/src/Tools/jEdit/patches/main Fri Aug 22 13:30:21 2025 +0200
+++ b/src/Tools/jEdit/patches/main Fri Aug 22 15:53:50 2025 +0200
@@ -969,9 +969,9 @@
+
private SyntaxUtilities(){}
}
-diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/EditPane.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/EditPane.java
+diff -Nru jedit5.7.0/jEdit/org/gjt/sp/jedit/EditPane.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/EditPane.java
--- jedit5.7.0/jEdit/org/gjt/sp/jedit/EditPane.java 2024-08-03 19:53:15.000000000 +0200
-+++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/EditPane.java 2025-05-14 15:46:36.934878462 +0200
++++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/EditPane.java 2025-08-22 13:25:05.602419198 +0200
@@ -43,6 +43,7 @@
import org.gjt.sp.jedit.msg.BufferChanging;
import org.gjt.sp.jedit.msg.BufferUpdate;
@@ -980,7 +980,15 @@
import org.gjt.sp.jedit.msg.PropertiesChanged;
import org.gjt.sp.jedit.options.GeneralOptionPane;
import org.gjt.sp.jedit.options.GutterOptionPane;
-@@ -380,9 +381,11 @@
+@@ -50,6 +51,7 @@
+ import org.gjt.sp.jedit.textarea.AntiAlias;
+ import org.gjt.sp.jedit.textarea.Gutter;
+ import org.gjt.sp.jedit.textarea.JEditTextArea;
++import org.gjt.sp.jedit.textarea.JEditTextAreaFactory;
+ import org.gjt.sp.jedit.textarea.MouseHandler;
+ import org.gjt.sp.jedit.textarea.Selection;
+ import org.gjt.sp.jedit.textarea.StatusListener;
+@@ -380,9 +382,11 @@
buffer.unsetProperty(Buffer.CARET_POSITIONED);
@@ -993,7 +1001,28 @@
// set any selections
Selection[] selection = caretInfo.selection;
-@@ -1029,7 +1032,7 @@
+@@ -756,7 +760,7 @@
+ //{{{ Package-private members
+
+ //{{{ EditPane constructor
+- EditPane(@Nonnull View view, @Nullable BufferSet bufferSetSource, @Nonnull Buffer buffer)
++ public EditPane(@Nonnull View view, @Nullable BufferSet bufferSetSource, @Nonnull Buffer buffer)
+ {
+ super(new BorderLayout());
+ BufferSet.Scope scope = jEdit.getBufferSetManager().getScope();
+@@ -795,7 +799,10 @@
+ this.view = view;
+
+
+- textArea = new JEditTextArea(view);
++ JEditTextAreaFactory textAreaFactory =
++ ServiceManager.getService(JEditTextAreaFactory.class, "textarea-factory");
++ textArea =
++ textAreaFactory == null ? new JEditTextArea(view) : textAreaFactory.create(view);
+ bufferSet.addBufferSetListener(this);
+ textArea.getPainter().setAntiAlias(new AntiAlias(jEdit.getProperty("view.antiAlias")));
+ textArea.setMouseHandler(new MouseHandler(textArea));
+@@ -1029,7 +1036,7 @@
for(int i = 0; i <= 3; i++)
{
foldLineStyle[i] = SyntaxUtilities.parseStyle(
@@ -1326,8 +1355,9 @@
// This is handled a little differently from other jEdit settings
// as this flag needs to be known very early in the
+diff -Nru jedit5.7.0/jEdit/org/gjt/sp/jedit/View.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/View.java
--- jedit5.7.0/jEdit/org/gjt/sp/jedit/View.java 2024-08-03 19:53:15.000000000 +0200
-+++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/View.java 2024-10-29 11:50:54.066016546 +0100
++++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/View.java 2025-08-22 13:22:50.795334674 +0200
@@ -1264,15 +1264,10 @@
StringBuilder title = new StringBuilder();
@@ -1348,3 +1378,46 @@
for(int i = 0; i < buffers.size(); i++)
{
+@@ -2070,7 +2065,11 @@
+
+ private EditPane createEditPane(@Nullable BufferSet bufferSetSource, @Nonnull Buffer buffer)
+ {
+- EditPane editPane = new EditPane(this, bufferSetSource, buffer);
++ EditPaneFactory editPaneFactory =
++ ServiceManager.getService(EditPaneFactory.class, "editpane-factory");
++ EditPane editPane =
++ editPaneFactory == null ? new EditPane(this, bufferSetSource, buffer) :
++ editPaneFactory.create(this, bufferSetSource, buffer);
+ JEditTextArea textArea = editPane.getTextArea();
+ textArea.addFocusListener(new FocusHandler());
+ textArea.addCaretListener(new CaretHandler());
+diff -Nru jedit5.7.0/jEdit/org/gjt/sp/jedit/EditPaneFactory.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/EditPaneFactory.java
+--- jedit5.7.0/jEdit/org/gjt/sp/jedit/EditPaneFactory.java 1970-01-01 01:00:00.000000000 +0100
++++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/EditPaneFactory.java 2025-08-22 13:21:29.596599634 +0200
+@@ -0,0 +1,11 @@
++package org.gjt.sp.jedit;
++
++import org.gjt.sp.jedit.bufferset.BufferSet;
++
++public class EditPaneFactory
++{
++ public EditPane create(View view, BufferSet bufferSetSource, Buffer buffer)
++ {
++ return new EditPane(view, bufferSetSource, buffer);
++ }
++}
+diff -Nru jedit5.7.0/jEdit/org/gjt/sp/jedit/textarea/JEditTextAreaFactory.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/textarea/JEditTextAreaFactory.java
+--- jedit5.7.0/jEdit/org/gjt/sp/jedit/textarea/JEditTextAreaFactory.java 1970-01-01 01:00:00.000000000 +0100
++++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/textarea/JEditTextAreaFactory.java 2025-08-22 13:21:51.268384088 +0200
+@@ -0,0 +1,11 @@
++package org.gjt.sp.jedit.textarea;
++
++import org.gjt.sp.jedit.View;
++
++public class JEditTextAreaFactory
++{
++ public JEditTextArea create(View view)
++ {
++ return new JEditTextArea(view);
++ }
++}