Browse Source

Tidy/fix double click detection in GUI simulator.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@5393 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 14 years ago
parent
commit
2b85d7307d
  1. 2
      prism/src/userinterface/simulator/GUISimulator.java

2
prism/src/userinterface/simulator/GUISimulator.java

@ -1869,7 +1869,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
public void doPopupDetection(MouseEvent e)
{
if (!computing) {
if (e.getClickCount() == 2 && e.getSource() == pathTablePlaceHolder || e.getSource() == tableScroll) {
if (e.getClickCount() == 2 && (e.getSource() == pathTablePlaceHolder || e.getSource() == tableScroll)) {
if (newPath.isEnabled())
a_newPath(false);
}

Loading…
Cancel
Save