--- a/src/Tools/jEdit/src/pretty_text_area.scala Thu Aug 11 13:23:00 2022 +0200
+++ b/src/Tools/jEdit/src/pretty_text_area.scala Fri Aug 12 11:18:22 2022 +0200
@@ -208,15 +208,15 @@
case KeyEvent.VK_C | KeyEvent.VK_INSERT
if strict_control && text_area.getSelectionCount != 0 =>
Registers.copy(text_area, '$')
- evt.consume
+ evt.consume()
case KeyEvent.VK_A
if strict_control =>
text_area.selectAll
- evt.consume
+ evt.consume()
case KeyEvent.VK_ESCAPE =>
- if (Isabelle.dismissed_popups(view)) evt.consume
+ if (Isabelle.dismissed_popups(view)) evt.consume()
case _ =>
}