Browse Source

Fixed bug where "backtrack to here" and "remove preceeding" where not disabled if the context menu popped up on the background

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@468 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Mark Kattenbelt 18 years ago
parent
commit
bd9f448b89
  1. 4
      prism/src/userinterface/simulator/GUISimulator.java

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

@ -1870,8 +1870,8 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
}
if(e.isPopupTrigger() && (e.getSource() == pathTablePlaceHolder || e.getSource() == pathTable || e.getSource() == pathTable.getTableHeader() || e.getSource() == tableScroll))
{
backtrackToHere.setEnabled(!(e.getSource() == pathTable.getTableHeader() || e.getSource() == pathTable.getParent()));
removeToHere.setEnabled(!(e.getSource() == pathTable.getTableHeader() || e.getSource() == pathTable.getParent()));
backtrackToHere.setEnabled(!(e.getSource() == pathTable.getTableHeader() || e.getSource() == pathTablePlaceHolder|| e.getSource() == tableScroll));
removeToHere.setEnabled(!(e.getSource() == pathTable.getTableHeader() || e.getSource() == pathTablePlaceHolder|| e.getSource() == tableScroll));
doEnables();

Loading…
Cancel
Save