equal
deleted
inserted
replaced
138 |
138 |
139 - Highlighting works via mouse hovering alone, without requiring |
139 - Highlighting works via mouse hovering alone, without requiring |
140 C-modifier. |
140 C-modifier. |
141 |
141 |
142 * An active highlight area in the input buffer or output panel may be |
142 * An active highlight area in the input buffer or output panel may be |
143 turned into a text selection by using the ALT modifier. Together with |
143 turned into a text selection by using the ALT modifier. |
144 SHIFT modifier, an existing selection is augmented (otherwise it is |
|
145 reset). |
|
146 |
144 |
147 * The "Documentation" panel supports plain text files again, notably |
145 * The "Documentation" panel supports plain text files again, notably |
148 "jedit-changes". This was broken in Isabelle2022, Isabelle2023, |
146 "jedit-changes". This was broken in Isabelle2022, Isabelle2023, |
149 Isabelle2024. |
147 Isabelle2024. |
150 |
148 |