--- a/src/Tools/Graphview/tree_panel.scala Wed Nov 13 23:11:06 2024 +0100
+++ b/src/Tools/Graphview/tree_panel.scala Thu Nov 14 10:50:49 2024 +0100
@@ -61,14 +61,15 @@
tree.addKeyListener(new KeyAdapter {
override def keyPressed(e: KeyEvent): Unit =
- if (e.getKeyCode == KeyEvent.VK_ENTER) {
+ if (!e.isConsumed() && e.getKeyCode == KeyEvent.VK_ENTER) {
e.consume()
selection_action()
}
})
tree.addMouseListener(new MouseAdapter {
override def mousePressed(e: MouseEvent): Unit =
- if (e.getClickCount == 2) {
+ if (!e.isConsumed() && e.getClickCount == 2) {
+ e.consume()
point_action(tree.getPathForLocation(e.getX, e.getY))
}
})
--- a/src/Tools/jEdit/src/completion_popup.scala Wed Nov 13 23:11:06 2024 +0100
+++ b/src/Tools/jEdit/src/completion_popup.scala Thu Nov 14 10:50:49 2024 +0100
@@ -629,8 +629,10 @@
list_view.peer.addMouseListener(new MouseAdapter {
override def mouseClicked(e: MouseEvent): Unit = {
- if (complete_selected()) e.consume()
- hide_popup()
+ if (!e.isConsumed()) {
+ if (complete_selected()) e.consume()
+ hide_popup()
+ }
}
})
--- a/src/Tools/jEdit/src/documentation_dockable.scala Wed Nov 13 23:11:06 2024 +0100
+++ b/src/Tools/jEdit/src/documentation_dockable.scala Thu Nov 14 10:50:49 2024 +0100
@@ -49,11 +49,16 @@
})
tree.addMouseListener(new MouseAdapter {
override def mouseClicked(e: MouseEvent): Unit = {
- val click = tree.getPathForLocation(e.getX, e.getY)
- if (click != null && e.getClickCount == 1) {
- val click_node = click.getLastPathComponent
- val path_node = tree.getLastSelectedPathComponent
- if (click_node == path_node) action(click_node)
+ if (!e.isConsumed()) {
+ val click = tree.getPathForLocation(e.getX, e.getY)
+ if (click != null && e.getClickCount == 1) {
+ val click_node = click.getLastPathComponent
+ val path_node = tree.getLastSelectedPathComponent
+ if (click_node == path_node) {
+ e.consume()
+ action(click_node)
+ }
+ }
}
}
})
--- a/src/Tools/jEdit/src/output_area.scala Wed Nov 13 23:11:06 2024 +0100
+++ b/src/Tools/jEdit/src/output_area.scala Thu Nov 14 10:50:49 2024 +0100
@@ -85,8 +85,13 @@
tree.addMouseListener(
new MouseAdapter {
override def mouseClicked(e: MouseEvent): Unit = {
- val click = tree.getPathForLocation(e.getX, e.getY)
- if (click != null && e.getClickCount == 1) handle_focus()
+ if (!e.isConsumed()) {
+ val click = tree.getPathForLocation(e.getX, e.getY)
+ if (click != null && e.getClickCount == 1) {
+ e.consume()
+ handle_focus()
+ }
+ }
}
})
--- a/src/Tools/jEdit/src/rich_text_area.scala Wed Nov 13 23:11:06 2024 +0100
+++ b/src/Tools/jEdit/src/rich_text_area.scala Thu Nov 14 10:50:49 2024 +0100
@@ -218,37 +218,39 @@
private val mouse_listener = new MouseAdapter {
override def mouseClicked(e: MouseEvent): Unit = {
robust_body(()) {
- val clicks = e.getClickCount
- if (clicks == 1) {
- hyperlink_area.info match {
- case Some(Text.Info(range, link)) =>
- if (!link.external) {
- try { text_area.moveCaretPosition(range.start) }
- catch {
- case _: ArrayIndexOutOfBoundsException =>
- case _: IllegalArgumentException =>
+ if (!e.isConsumed()) {
+ val clicks = e.getClickCount
+ if (clicks == 1) {
+ hyperlink_area.info match {
+ case Some(Text.Info(range, link)) =>
+ if (!link.external) {
+ try { text_area.moveCaretPosition(range.start) }
+ catch {
+ case _: ArrayIndexOutOfBoundsException =>
+ case _: IllegalArgumentException =>
+ }
+ text_area.requestFocus()
}
- text_area.requestFocus()
- }
- link.follow(view)
- e.consume()
- case None =>
+ link.follow(view)
+ e.consume()
+ case None =>
+ }
+ active_area.text_info match {
+ case Some((text, Text.Info(_, markup))) =>
+ Active.action(view, text, markup)
+ close_action()
+ e.consume()
+ case None =>
+ }
}
- active_area.text_info match {
- case Some((text, Text.Info(_, markup))) =>
- Active.action(view, text, markup)
- close_action()
- e.consume()
- case None =>
- }
- }
- else if (clicks == 2) {
- highlight_area.info match {
- case Some(Text.Info(r, _)) =>
- text_area.selectNone()
- text_area.addToSelection(new Selection.Range(r.start, r.stop))
- e.consume()
- case None =>
+ else if (clicks == 2) {
+ highlight_area.info match {
+ case Some(Text.Info(r, _)) =>
+ text_area.selectNone()
+ text_area.addToSelection(new Selection.Range(r.start, r.stop))
+ e.consume()
+ case None =>
+ }
}
}
}
--- a/src/Tools/jEdit/src/status_widget.scala Wed Nov 13 23:11:06 2024 +0100
+++ b/src/Tools/jEdit/src/status_widget.scala Thu Nov 14 10:50:49 2024 +0100
@@ -87,7 +87,8 @@
addMouseListener(new MouseAdapter {
override def mouseClicked(evt: MouseEvent): Unit = {
- if (evt.getClickCount == 2) {
+ if (!evt.isConsumed() && evt.getClickCount == 2) {
+ evt.consume()
view.getInputHandler.invokeAction(action)
}
}
--- a/src/Tools/jEdit/src/text_overview.scala Wed Nov 13 23:11:06 2024 +0100
+++ b/src/Tools/jEdit/src/text_overview.scala Thu Nov 14 10:50:49 2024 +0100
@@ -33,9 +33,13 @@
addMouseListener(new MouseAdapter {
override def mousePressed(event: MouseEvent): Unit = {
- val line = (event.getY * lines()) / getHeight
- if (line >= 0 && line < text_area.getLineCount)
- text_area.setCaretPosition(text_area.getLineStartOffset(line))
+ if (!event.isConsumed()) {
+ val line = (event.getY * lines()) / getHeight
+ if (line >= 0 && line < text_area.getLineCount) {
+ event.consume()
+ text_area.setCaretPosition(text_area.getLineStartOffset(line))
+ }
+ }
}
})