Merge lp:~tapaal-contributor/tapaal/interrupted-scrolling-1938783 into lp:tapaal

[Lena Ernstsen]

Scroll will not be interrupted by arcs anymore

When hitting an arc or arc point while scrolling it will not halt

[Kenneth Yrke Jørgensen (yrke)]

review: Approve (code)

[Jiri Srba (srba)]

tested and works

review: Approve

=== modified file 'src/dk/aau/cs/gui/TabContent.java'
--- src/dk/aau/cs/gui/TabContent.java	2021-07-27 12:51:40 +0000
+++ src/dk/aau/cs/gui/TabContent.java	2021-08-04 11:22:35 +0000
@@ -2760,7 +2760,18 @@
                 e->e.pno instanceof TimedTransitionComponent && e.a == MouseAction.wheel,
                 e->timedTranstionMouseWheelWithShift(((TimedTransitionComponent) e.pno), ((MouseWheelEvent) e.e))
             );
+            registerEvent(
+                e->e.pno instanceof Arc && e.a == MouseAction.wheel,
+                e->arcMouseWheel((PetriNetObject) e.pno, e.e)
+            );
+            registerEvent(
+                e->e.pno instanceof ArcPathPoint && e.a == MouseAction.wheel,
+                e->arcMouseWheel(((PetriNetObject) e.pno), e.e)
+            );
+        }
 
+        private void arcMouseWheel(PetriNetObject pno, MouseEvent e) {
+            pno.getParent().dispatchEvent(e);
         }
 
         private void timedTranstionMouseWheelWithShift(TimedTransitionComponent p, MouseWheelEvent e) {