--- a/src/Tools/Graphview/tree_panel.scala Thu Aug 11 13:23:00 2022 +0200
+++ b/src/Tools/Graphview/tree_panel.scala Fri Aug 12 11:18:22 2022 +0200
@@ -73,7 +73,7 @@
tree.addKeyListener(new KeyAdapter {
override def keyPressed(e: KeyEvent): Unit =
if (e.getKeyCode == KeyEvent.VK_ENTER) {
- e.consume
+ e.consume()
selection_action()
}
})
--- a/src/Tools/jEdit/src/completion_popup.scala Thu Aug 11 13:23:00 2022 +0200
+++ b/src/Tools/jEdit/src/completion_popup.scala Fri Aug 12 11:18:22 2022 +0200
@@ -517,12 +517,12 @@
case KeyEvent.KEY_PRESSED =>
val key_code = evt.getKeyCode
if (key_code == KeyEvent.VK_ESCAPE) {
- if (dismissed()) evt.consume
+ if (dismissed()) evt.consume()
}
case KeyEvent.KEY_TYPED =>
super.processKeyEvent(evt)
process(evt)
- evt.consume
+ evt.consume()
case _ =>
}
if (!evt.isConsumed) super.processKeyEvent(evt)
@@ -598,26 +598,26 @@
if (!e.isConsumed) {
e.getKeyCode match {
case KeyEvent.VK_ENTER if PIDE.options.bool("jedit_completion_select_enter") =>
- if (complete_selected()) e.consume
+ if (complete_selected()) e.consume()
hide_popup()
case KeyEvent.VK_TAB if PIDE.options.bool("jedit_completion_select_tab") =>
- if (complete_selected()) e.consume
+ if (complete_selected()) e.consume()
hide_popup()
case KeyEvent.VK_ESCAPE =>
hide_popup()
- e.consume
+ e.consume()
case KeyEvent.VK_UP | KeyEvent.VK_KP_UP if multi =>
move_items(-1)
- e.consume
+ e.consume()
case KeyEvent.VK_DOWN | KeyEvent.VK_KP_DOWN if multi =>
move_items(1)
- e.consume
+ e.consume()
case KeyEvent.VK_PAGE_UP if multi =>
move_pages(-1)
- e.consume
+ e.consume()
case KeyEvent.VK_PAGE_DOWN if multi =>
move_pages(1)
- e.consume
+ e.consume()
case _ =>
if (e.isActionKey || e.isAltDown || e.isMetaDown || e.isControlDown)
hide_popup()
@@ -632,7 +632,7 @@
list_view.peer.addMouseListener(new MouseAdapter {
override def mouseClicked(e: MouseEvent): Unit = {
- if (complete_selected()) e.consume
+ if (complete_selected()) e.consume()
hide_popup()
}
})
--- a/src/Tools/jEdit/src/document_view.scala Thu Aug 11 13:23:00 2022 +0200
+++ b/src/Tools/jEdit/src/document_view.scala Fri Aug 12 11:18:22 2022 +0200
@@ -177,7 +177,7 @@
JEdit_Lib.key_listener(
key_pressed = { (evt: KeyEvent) =>
if (evt.getKeyCode == KeyEvent.VK_ESCAPE && Isabelle.dismissed_popups(text_area.getView)) {
- evt.consume
+ evt.consume()
}
}
)
--- a/src/Tools/jEdit/src/documentation_dockable.scala Thu Aug 11 13:23:00 2022 +0200
+++ b/src/Tools/jEdit/src/documentation_dockable.scala Fri Aug 12 11:18:22 2022 +0200
@@ -58,7 +58,7 @@
tree.addKeyListener(new KeyAdapter {
override def keyPressed(e: KeyEvent): Unit = {
if (e.getKeyCode == KeyEvent.VK_ENTER) {
- e.consume
+ e.consume()
val path = tree.getSelectionPath
if (path != null) {
path.getLastPathComponent match {
--- 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 _ =>
}
--- a/src/Tools/jEdit/src/query_dockable.scala Thu Aug 11 13:23:00 2022 +0200
+++ b/src/Tools/jEdit/src/query_dockable.scala Fri Aug 12 11:18:22 2022 +0200
@@ -243,7 +243,7 @@
reactions += {
case ButtonClicked(_) => apply_query()
case evt @ KeyPressed(_, Key.Enter, 0, _) =>
- evt.peer.consume
+ evt.peer.consume()
apply_query()
}
}