# HG changeset patch
# User wenzelm
# Date 1731069745 -3600
# Node ID 4a62c57fe7459bb446de878056024400f23f72af
# Parent  6b805c746e3bfafeb013e833dedd34206b8cdfd4
tuned signature;

diff -r 6b805c746e3b -r 4a62c57fe745 src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Fri Nov 08 13:37:13 2024 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Fri Nov 08 13:42:25 2024 +0100
@@ -32,7 +32,7 @@
   close_action: () => Unit = () => (),
   propagate_keys: Boolean = false
 ) extends JEditEmbeddedTextArea {
-  text_area =>
+  pretty_text_area =>
 
   GUI_Thread.require {}
 
@@ -45,7 +45,7 @@
   private var future_refresh: Option[Future[Unit]] = None
 
   private val rich_text_area =
-    new Rich_Text_Area(view, text_area, () => current_rendering, close_action,
+    new Rich_Text_Area(view, pretty_text_area, () => current_rendering, close_action,
       get_search_pattern _, () => (), caret_visible = false, enable_hovering = true)
 
   private var current_search_pattern: Option[Regex] = None
@@ -176,7 +176,7 @@
       }
     if (current_search_pattern != pattern) {
       current_search_pattern = pattern
-      text_area.getPainter.repaint()
+      pretty_text_area.getPainter.repaint()
     }
     text_field.setForeground(
       if (ok) search_field_foreground
@@ -205,9 +205,9 @@
   override def getInputMethodRequests: InputMethodRequests = null
 
   inputHandlerProvider =
-    new DefaultInputHandlerProvider(new TextAreaInputHandler(text_area) {
+    new DefaultInputHandlerProvider(new TextAreaInputHandler(pretty_text_area) {
       override def getAction(action: String): JEditBeanShellAction =
-        text_area.getActionContext.getAction(action)
+        pretty_text_area.getActionContext.getAction(action)
       override def processKeyEvent(evt: KeyEvent, from: Int, global: Boolean): Unit = {}
       override def handleKey(key: KeyEventTranslator.Key, dry_run: Boolean): Boolean = false
     })
@@ -219,13 +219,13 @@
 
       evt.getKeyCode match {
         case KeyEvent.VK_C | KeyEvent.VK_INSERT
-        if strict_control && text_area.getSelectionCount != 0 =>
-          Registers.copy(text_area, '$')
+        if strict_control && pretty_text_area.getSelectionCount != 0 =>
+          Registers.copy(pretty_text_area, '$')
           evt.consume()
 
         case KeyEvent.VK_A
         if strict_control =>
-          text_area.selectAll()
+          pretty_text_area.selectAll()
           evt.consume()
 
         case KeyEvent.VK_ESCAPE =>