# HG changeset patch
# User wenzelm
# Date 1731683066 -3600
# Node ID cc9fc6f375b24a0b745a747fa3c37e5dc3ae5af7
# Parent  0c29878ae48fdc9f891da050cbf139830d17ce09
proper focus to support subsequent copy-paste via keyboard;

diff -r 0c29878ae48f -r cc9fc6f375b2 src/Tools/jEdit/src/rich_text_area.scala
--- a/src/Tools/jEdit/src/rich_text_area.scala	Fri Nov 15 16:01:41 2024 +0100
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Fri Nov 15 16:04:26 2024 +0100
@@ -285,6 +285,7 @@
                 if (JEdit_Lib.alt_modifier(evt)) {
                   highlight_area.info.map(_.range) match {
                     case Some(range) =>
+                      text_area.requestFocus()
                       text_area.selectNone()
                       text_area.addToSelection(new Selection.Range(range.start, range.stop))
                     case None =>