Merge lp:~tapaal-developers/tapaal/fix-915296-disableRename into lp:tapaal

[Kenneth Yrke Jørgensen]

Merged branch to fix bug #915296

Fix bug 915296 where the disable rename and remove buttons in the shared transition/places was not disabled when there where no element in the list.

[Jiri Srba (srba)]

The problem is solved for shared places. However, if you switch to shared transitions,
create one and delete, the rename and remove buttons are still enabled.

review: Needs Fixing

[lp:~tapaal-developers/tapaal/fix-915296-disableRename]

679. By Kenneth Yrke Jørgensen on 2012-03-08

Now also fixed bug #915296 for shared transitions and when moving between
shared transitions and shared places.

[Jiri Srba (srba)]

review: Approve

=== modified file 'src/dk/aau/cs/gui/SharedPlacesAndTransitionsPanel.java'
--- src/dk/aau/cs/gui/SharedPlacesAndTransitionsPanel.java	2012-02-17 19:48:41 +0000
+++ src/dk/aau/cs/gui/SharedPlacesAndTransitionsPanel.java	2012-03-08 07:56:17 +0000
@@ -298,6 +298,10 @@
 					moveDownButton.setEnabled(false);
 					moveUpButton.setEnabled(false);
 				}
+				if (list.getModel().getSize() <= 0){
+					renameButton.setEnabled(false);
+					removeButton.setEnabled(false);
+				}
 			}		
 		});
 		placesTransitionsComboBox.setSelectedIndex(0); // Sets up the proper list model
@@ -624,6 +628,15 @@
 		public void removeElement(SharedPlace place) {
 			network.remove(place);
 			fireContentsChanged(this, 0, getSize());
+			int numElements = list.getModel().getSize();
+			if(numElements <= 1) {
+				moveDownButton.setEnabled(false);
+				moveUpButton.setEnabled(false);
+			}
+			if (numElements <= 0) {
+				removeButton.setEnabled(false);
+				renameButton.setEnabled(false);
+			}
 		}
 
 		public void updatedName(){
@@ -694,6 +707,15 @@
 		public void removeElement(SharedTransition transition) {
 			network.remove(transition);
 			fireContentsChanged(this, 0, getSize());
+			int numElements = list.getModel().getSize();
+			if(numElements <= 1) {
+				moveDownButton.setEnabled(false);
+				moveUpButton.setEnabled(false);
+			}
+			if (numElements <= 0) {
+				removeButton.setEnabled(false);
+				renameButton.setEnabled(false);
+			}
 		}
 
 		public void updatedName() {