pro-forma use of ViewFactory and TextAreaPainterFactory;

--- a/src/Tools/jEdit/jedit_base/services.xml	Sat Aug 23 20:34:37 2025 +0200
+++ b/src/Tools/jEdit/jedit_base/services.xml	Sat Aug 23 13:47:40 2025 +0200
@@ -5,12 +5,18 @@
   <SERVICE NAME="UTF-8-Isabelle" CLASS="org.gjt.sp.jedit.io.Encoding">
     new isabelle.jedit.Isabelle_Encoding();
   </SERVICE>
+  <SERVICE CLASS="org.gjt.sp.jedit.ViewFactory" NAME="view-factory">
+    new isabelle.jedit.JEdit_Accessible$View_Factory();
+  </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.textarea.TextAreaPainterFactory" NAME="painter-factory">
+    new isabelle.jedit.JEdit_Accessible$Painter_Factory();
+  </SERVICE>
   <SERVICE CLASS="org.gjt.sp.jedit.gui.DockingFrameworkProvider" NAME="PIDE">
     new isabelle.jedit.PIDE_Docking_Framework();
   </SERVICE>

--- a/src/Tools/jEdit/src/jedit_accessible.scala	Sat Aug 23 20:34:37 2025 +0200
+++ b/src/Tools/jEdit/src/jedit_accessible.scala	Sat Aug 23 13:47:40 2025 +0200
@@ -12,9 +12,10 @@
 import isabelle._
 
 import org.gjt.sp.jedit
-import org.gjt.sp.jedit.{Buffer, View}
+import org.gjt.sp.jedit.{Buffer, ViewFactory}
 import org.gjt.sp.jedit.bufferset.BufferSet
-import org.gjt.sp.jedit.textarea.{JEditTextArea, JEditTextAreaFactory}
+import org.gjt.sp.jedit.textarea.{JEditTextArea, JEditTextAreaFactory, TextArea => TextArea_JEdit,
+  TextAreaPainter, TextAreaPainterFactory}
 
 import java.awt.{Point, Rectangle}
 import javax.accessibility.{Accessible, AccessibleContext, AccessibleRole, AccessibleText}
@@ -23,15 +24,33 @@
 
 
 object JEdit_Accessible {
+  /* view */
+
+  class View_Factory extends ViewFactory {
+    override def create(buffer: Buffer, config: jedit.View.ViewConfig): jedit.View =
+      new View(buffer, config)
+  }
+
+  class View(buffer: Buffer, config: jedit.View.ViewConfig) extends jedit.View(buffer, config) {
+    override def getAccessibleContext: AccessibleContext = {
+      if (accessibleContext == null) { accessibleContext = new Accessible_Context }
+      accessibleContext
+    }
+
+    class Accessible_Context extends AccessibleJFrame {
+    }
+  }
+
+
   /* editpane */
 
   class EditPane_Factory extends jedit.EditPaneFactory {
-    override def create(view: View, bufferSetSource: BufferSet, buffer: Buffer): jedit.EditPane =
+    override def create(view: jedit.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) {
+  class EditPane(view: jedit.View, bufferSetSource: BufferSet, buffer: Buffer)
+      extends jedit.EditPane(view: jedit.View, bufferSetSource: BufferSet, buffer: Buffer) {
     override def getAccessibleContext: AccessibleContext = {
       if (accessibleContext == null) { accessibleContext = new Accessible_Context }
       accessibleContext
@@ -46,10 +65,10 @@
   /* textarea */
 
   class TextArea_Factory extends JEditTextAreaFactory {
-    override def create(view: View): JEditTextArea = new TextArea(view)
+    override def create(view: jedit.View): JEditTextArea = new TextArea(view)
   }
 
-  class TextArea(view: View) extends JEditTextArea(view: View) {
+  class TextArea(view: jedit.View) extends JEditTextArea(view: jedit.View) {
     text_area =>
 
     override def getAccessibleContext: AccessibleContext = {
@@ -137,4 +156,23 @@
         else ""
     }
   }
+
+
+  /* text area painter */
+
+  class Painter_Factory extends TextAreaPainterFactory {
+    override def create(text_area: TextArea_JEdit): TextAreaPainter = new Painter(text_area)
+  }
+
+  class Painter(text_area: TextArea_JEdit) extends TextAreaPainter(text_area) {
+    override def getAccessibleContext: AccessibleContext = {
+      if (accessibleContext == null) {
+        accessibleContext = new Accessible_Context
+      }
+      accessibleContext
+    }
+
+    class Accessible_Context extends AccessibleJComponent {
+    }
+  }
 }