--- a/NEWS Thu Nov 14 10:50:49 2024 +0100
+++ b/NEWS Thu Nov 14 11:12:11 2024 +0100
@@ -137,10 +137,12 @@
with less load on the GUI thread.
- Highlighting works via mouse hovering alone, without requiring
- C-modifier. Double click selects that area.
+ C-modifier.
* An active highlight area in the input buffer or output panel may be
-selected via double-click.
+turned into a text selection by using the ALT modifier. Together with
+SHIFT modifier, an existing selection is augmented (otherwise it is
+reset).
* The "Documentation" panel supports plain text files again, notably
"jedit-changes". This was broken in Isabelle2022, Isabelle2023,