# HG changeset patch
# User wenzelm
# Date 1731672528 -3600
# Node ID 7a7ad99212b17b1dc491576ab5b74a401fce8435
# Parent  82110cbcf9a1d0874cbceaa4a72a0aa01108a623
less ambitious selection;

diff -r 82110cbcf9a1 -r 7a7ad99212b1 NEWS
--- a/NEWS	Thu Nov 14 11:33:51 2024 +0100
+++ b/NEWS	Fri Nov 15 13:08:48 2024 +0100
@@ -140,9 +140,7 @@
     C-modifier.
 
 * An active highlight area in the input buffer or output panel may be
-turned into a text selection by using the ALT modifier. Together with
-SHIFT modifier, an existing selection is augmented (otherwise it is
-reset).
+turned into a text selection by using the ALT modifier.
 
 * The "Documentation" panel supports plain text files again, notably
 "jedit-changes". This was broken in Isabelle2022, Isabelle2023,
diff -r 82110cbcf9a1 -r 7a7ad99212b1 src/Tools/jEdit/src/rich_text_area.scala
--- a/src/Tools/jEdit/src/rich_text_area.scala	Thu Nov 14 11:33:51 2024 +0100
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Fri Nov 15 13:08:48 2024 +0100
@@ -285,7 +285,7 @@
                 if (JEdit_Lib.alt_modifier(evt)) {
                   highlight_area.info.map(_.range) match {
                     case Some(range) =>
-                      if (!JEdit_Lib.shift_modifier(evt)) text_area.selectNone()
+                      text_area.selectNone()
                       text_area.addToSelection(new Selection.Range(range.start, range.stop))
                     case None =>
                   }