Browse Source

Bugfix: Can now edit invalid properties in GUI.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@182 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 19 years ago
parent
commit
9a56953fd5
  1. 8
      prism/src/userinterface/properties/GUIMultiProperties.java

8
prism/src/userinterface/properties/GUIMultiProperties.java

@ -598,7 +598,7 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List
// properties list
propList.setEnabled (!computing);
newProperty.setEnabled (!computing);
editProperty.setEnabled (!computing && propList.getValidSelectedProperties().size() > 0);
editProperty.setEnabled (!computing && propList.getSelectedProperties().size() > 0);
cutAction.setEnabled (!computing);
copyAction.setEnabled (!computing);
pasteAction.setEnabled (!computing);
@ -1324,7 +1324,7 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List
verifySelected.setEnabled(propList.getValidSelectedProperties().size() > 0);
simulate.setEnabled(propList.getValidSimulatableSelectedProperties().size() > 0);
details.setEnabled(propList.getValidSelectedProperties().size() > 0);
editProperty.setEnabled(propList.getValidSelectedProperties().size() > 0);
editProperty.setEnabled(propList.getSelectedProperties().size() > 0);
newExperiment.setEnabled(propList.getNumSelectedProperties() == 1 && propList.getValidSelectedProperties().size() == 1);
@ -1410,7 +1410,7 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List
verifySelected.setEnabled(propList.getValidSelectedProperties().size() > 0);
simulate.setEnabled(propList.getValidSimulatableSelectedProperties().size() > 0);
details.setEnabled(propList.getValidSelectedProperties().size() > 0);
editProperty.setEnabled(propList.getValidSelectedProperties().size() > 0);
editProperty.setEnabled(propList.getSelectedProperties().size() > 0);
newExperiment.setEnabled(propList.getNumSelectedProperties() == 1 && propList.getValidSelectedProperties().size() == 1);
if(showDeleters == false)
@ -1463,7 +1463,7 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List
verifySelected.setEnabled(propList.getValidSelectedProperties().size() > 0);
simulate.setEnabled(propList.getValidSimulatableSelectedProperties().size() > 0);
details.setEnabled(propList.getValidSelectedProperties().size() > 0);
editProperty.setEnabled(propList.getValidSelectedProperties().size() > 0);
editProperty.setEnabled(propList.getSelectedProperties().size() > 0);
if(showDeleters == false)
{
cutAction.setEnabled(false);

Loading…
Cancel
Save