--- a/Admin/components/components.sha1 Fri Aug 22 16:54:33 2025 +0100
+++ b/Admin/components/components.sha1 Fri Aug 22 22:45:30 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 16:54:33 2025 +0100
+++ b/Admin/components/main Fri Aug 22 22:45:30 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/etc/build.props Fri Aug 22 16:54:33 2025 +0100
+++ b/etc/build.props Fri Aug 22 22:45:30 2025 +0200
@@ -311,6 +311,7 @@
src/Tools/jEdit/src/isabelle_navigator.scala \
src/Tools/jEdit/src/isabelle_session.scala \
src/Tools/jEdit/src/isabelle_vfs.scala \
+ src/Tools/jEdit/src/jedit_accessible.scala \
src/Tools/jEdit/src/jedit_bibtex.scala \
src/Tools/jEdit/src/jedit_editor.scala \
src/Tools/jEdit/src/jedit_jar.scala \
--- a/src/Pure/GUI/tree_view.scala Fri Aug 22 16:54:33 2025 +0100
+++ b/src/Pure/GUI/tree_view.scala Fri Aug 22 22:45:30 2025 +0200
@@ -6,6 +6,8 @@
package isabelle
+import javax.accessibility.AccessibleContext
+
import javax.swing.JTree
import javax.swing.tree.{MutableTreeNode, DefaultMutableTreeNode, DefaultTreeModel,
TreeSelectionModel, DefaultTreeCellRenderer}
@@ -46,9 +48,19 @@
class Tree_View(
val root: Tree_View.Node = Tree_View.Node(),
- single_selection_mode: Boolean = false
+ single_selection_mode: Boolean = false,
+ accessible_name: String = ""
) extends JTree(root) {
- getAccessibleContext.setAccessibleName(root.toString)
+
+ override def getAccessibleContext: AccessibleContext = {
+ if (accessibleContext == null) { accessibleContext = new Accessible_Context }
+ accessibleContext
+ }
+ class Accessible_Context extends AccessibleJTree {
+ override def getAccessibleName: String =
+ proper_string(accessible_name).getOrElse(proper_string(root.toString).orNull)
+ }
+
def get_selection[A](which: PartialFunction[AnyRef, A]): Option[A] =
getLastSelectedPathComponent match {
case Tree_View.Node(obj) if obj != null && which.isDefinedAt(obj) => Some(which(obj))
--- a/src/Pure/General/untyped.scala Fri Aug 22 16:54:33 2025 +0100
+++ b/src/Pure/General/untyped.scala Fri Aug 22 22:45:30 2025 +0200
@@ -17,7 +17,7 @@
con
}
- def the_constructor[C](c: Class[C]): Constructor[C] = {
+ def the_constructor[C](c: Class[C]): Constructor[C] = {
c.getDeclaredConstructors().toList match {
case List(con) =>
con.setAccessible(true)
--- a/src/Tools/jEdit/jedit_base/services.xml Fri Aug 22 16:54:33 2025 +0100
+++ b/src/Tools/jEdit/jedit_base/services.xml Fri Aug 22 22:45:30 2025 +0200
@@ -5,6 +5,12 @@
<SERVICE NAME="UTF-8-Isabelle" CLASS="org.gjt.sp.jedit.io.Encoding">
new isabelle.jedit.Isabelle_Encoding();
</SERVICE>
+ <SERVICE CLASS="org.gjt.sp.jedit.EditPaneFactory" NAME="editpane-factory">
+ new isabelle.jedit.JEdit_Accessible$EditPane_Factory();
+ </SERVICE>
+ <SERVICE CLASS="org.gjt.sp.jedit.textarea.JEditTextAreaFactory" NAME="textarea-factory">
+ new isabelle.jedit.JEdit_Accessible$TextArea_Factory();
+ </SERVICE>
<SERVICE CLASS="org.gjt.sp.jedit.gui.DockingFrameworkProvider" NAME="PIDE">
new isabelle.jedit.PIDE_Docking_Framework();
</SERVICE>
--- a/src/Tools/jEdit/patches/main Fri Aug 22 16:54:33 2025 +0100
+++ b/src/Tools/jEdit/patches/main Fri Aug 22 22:45:30 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,3 +1355,69 @@
// 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 2025-08-22 13:22:50.795334674 +0200
+@@ -1264,15 +1264,10 @@
+
+ StringBuilder title = new StringBuilder();
+
+- /* On Mac OS X, apps are not supposed to show their name in the
+- title bar. */
+- if(!OperatingSystem.isMacOS())
+- {
+- if (userTitle != null)
+- title.append(userTitle);
+- else
+- title.append(jEdit.getProperty("view.title"));
+- }
++ if (userTitle != null)
++ title.append(userTitle);
++ else
++ title.append(jEdit.getProperty("view.title"));
+
+ 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);
++ }
++}
--- a/src/Tools/jEdit/patches/title Fri Aug 22 16:54:33 2025 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,22 +0,0 @@
---- 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
-@@ -1264,15 +1264,10 @@
-
- StringBuilder title = new StringBuilder();
-
-- /* On Mac OS X, apps are not supposed to show their name in the
-- title bar. */
-- if(!OperatingSystem.isMacOS())
-- {
-- if (userTitle != null)
-- title.append(userTitle);
-- else
-- title.append(jEdit.getProperty("view.title"));
-- }
-+ if (userTitle != null)
-+ title.append(userTitle);
-+ else
-+ title.append(jEdit.getProperty("view.title"));
-
- for(int i = 0; i < buffers.size(); i++)
- {
--- a/src/Tools/jEdit/src/documentation_dockable.scala Fri Aug 22 16:54:33 2025 +0100
+++ b/src/Tools/jEdit/src/documentation_dockable.scala Fri Aug 22 22:45:30 2025 +0200
@@ -19,8 +19,7 @@
class Documentation_Dockable(view: View, position: String) extends Dockable(view, position) {
private val doc_contents = Doc.contents(PIDE.ml_settings)
- private val tree = new Tree_View(single_selection_mode = true)
- tree.getAccessibleContext.setAccessibleName("Documentation")
+ private val tree = new Tree_View(single_selection_mode = true, accessible_name = "Documentation")
for (section <- doc_contents.sections) {
tree.root.add(Tree_View.Node(section.title))
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/jedit_accessible.scala Fri Aug 22 22:45:30 2025 +0200
@@ -0,0 +1,140 @@
+/* Title: Tools/jEdit/src/jedit_accessible.scala
+ Author: Makarius
+
+Support for accessible jEdit components, notably used with screenreaders:
+ - Windows: NVDA (see https://www.nvaccess.org)
+ - macOS: VoiceOver (builtin Command-F5)
+*/
+
+package isabelle.jedit
+
+
+import isabelle._
+
+import org.gjt.sp.jedit
+import org.gjt.sp.jedit.{Buffer, View}
+import org.gjt.sp.jedit.bufferset.BufferSet
+import org.gjt.sp.jedit.textarea.{JEditTextArea, JEditTextAreaFactory}
+
+import java.awt.{Point, Rectangle}
+import javax.accessibility.{Accessible, AccessibleContext, AccessibleRole, AccessibleText}
+import javax.swing.{JPanel, SwingUtilities}
+import javax.swing.text.{AttributeSet, SimpleAttributeSet}
+
+
+object JEdit_Accessible {
+ /* editpane */
+
+ class EditPane_Factory extends jedit.EditPaneFactory {
+ override def create(view: View, bufferSetSource: BufferSet, buffer: Buffer): jedit.EditPane =
+ new EditPane(view, bufferSetSource, buffer)
+ }
+
+ class EditPane(view: View, bufferSetSource: BufferSet, buffer: Buffer)
+ extends jedit.EditPane(view: View, bufferSetSource: BufferSet, buffer: Buffer) {
+ override def getAccessibleContext: AccessibleContext = {
+ if (accessibleContext == null) { accessibleContext = new Accessible_Context }
+ accessibleContext
+ }
+
+ class Accessible_Context extends AccessibleJPanel {
+ override def getAccessibleName: String = "editor panel"
+ }
+ }
+
+
+ /* textarea */
+
+ class TextArea_Factory extends JEditTextAreaFactory {
+ override def create(view: View): JEditTextArea = new TextArea(view)
+ }
+
+ class TextArea(view: View) extends JEditTextArea(view: View) {
+ text_area =>
+
+ override def getAccessibleContext: AccessibleContext = {
+ if (accessibleContext == null) { accessibleContext = new Accessible_Context }
+ accessibleContext
+ }
+
+ protected class Accessible_Context extends AccessibleJPanel {
+ override def getAccessibleName: String = "editor text"
+ override def getAccessibleRole: AccessibleRole = AccessibleRole.TEXT
+ override def getAccessibleText: AccessibleText = accessible_text
+ override def getAccessibleChildrenCount: Int = 0
+ override def getAccessibleChild(i: Int): Accessible = null
+ }
+
+ protected val accessible_text: AccessibleText = new Accessible_Text
+
+ protected class Accessible_Text extends AccessibleText {
+ private def get_character(i: Text.Offset, inc: Int = 0): Option[Text.Info[String]] =
+ JEdit_Lib.buffer_lock(buffer) {
+ val range0 = JEdit_Lib.point_range(buffer, i)
+ val range =
+ if (inc == 0) range0
+ else JEdit_Lib.point_range(buffer, if (inc > 0) range0.stop else range0.start - 1)
+ JEdit_Lib.get_text(buffer, range).map(Text.Info(range, _))
+ }
+
+ override def getIndexAtPoint(p: Point): Int = {
+ val q = SwingUtilities.convertPoint(text_area, p, painter)
+ text_area.xyToOffset(q.x, q.y)
+ }
+
+ override def getCharacterBounds(index: Int): Rectangle =
+ (for {
+ info <- get_character(index)
+ gfx <- JEdit_Lib.gfx_range(text_area)(info.range)
+ }
+ yield {
+ val r = new Rectangle(gfx.x, gfx.y, gfx.length, painter.getLineHeight)
+ SwingUtilities.convertRectangle(painter, r, text_area)
+ }).getOrElse(new Rectangle())
+
+ override def getCharCount: Int = text_area.getBufferLength
+
+ override def getCaretPosition: Int = text_area.getCaretPosition
+
+ override def getAtIndex(part: Int, index: Int): String =
+ part match {
+ case AccessibleText.CHARACTER =>
+ get_character(index).map(_.info).orNull
+ case _ => null
+ }
+
+ override def getAfterIndex(part: Int, index: Int): String =
+ part match {
+ case AccessibleText.CHARACTER =>
+ get_character(index, inc = 1).map(_.info).orNull
+ case _ => null
+ }
+
+ override def getBeforeIndex(part: Int, index: Int): String =
+ part match {
+ case AccessibleText.CHARACTER =>
+ get_character(index, inc = -1).map(_.info).orNull
+ case _ => null
+ }
+
+ override def getCharacterAttribute(i: Int): AttributeSet =
+ SimpleAttributeSet.EMPTY
+
+ override def getSelectionStart: Int =
+ if (text_area.getSelectionCount == 1) text_area.getSelection(0).getStart
+ else -1
+
+ override def getSelectionEnd: Int =
+ if (text_area.getSelectionCount == 1) text_area.getSelection(0).getEnd
+ else -1
+
+ override def getSelectedText: String =
+ if (text_area.getSelectionCount == 1) {
+ val start = getSelectionStart
+ val stop = getSelectionEnd
+ buffer.getText(start, stop - start)
+ }
+ else ""
+ }
+ }
+}