proper focus to support subsequent copy-paste via keyboard;

--- 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 =>