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