Merge lp:~tapaal-contributor/tapaal/edit-interval-1940402 into lp:tapaal

[Lena Ernstsen]

Fixed not being able to edit right part of intervals

[Jiri Srba (srba)]

tested and fixes the problem

review: Approve

=== modified file 'src/pipe/gui/widgets/GuardDialogue.java'
--- src/pipe/gui/widgets/GuardDialogue.java	2021-04-08 08:30:29 +0000
+++ src/pipe/gui/widgets/GuardDialogue.java	2021-08-24 09:34:51 +0000
@@ -561,7 +561,7 @@
 			rightDelimiter.setEnabled(true);
 		else
 			rightDelimiter.setEnabled(!inf.isSelected());
-		secondIntervalNumber.setVisible(!value);
+        secondIntervalNumber.setVisible(!value);
 		rightConstantsComboBox.setVisible(value);
 
 		repackIfWindow();
@@ -671,31 +671,33 @@
 		String oldRight = rightConstantsComboBox.getSelectedItem() != null ? rightConstantsComboBox
 				.getSelectedItem().toString()
 				: null;
-				rightConstantsComboBox.removeAllItems();
-				Collection<Constant> constants = CreateGui.getCurrentTab().network()
-				.constants();
-				
-				//List <Constant> constantList = new ArrayList(constants);
-				List <Constant> constantList = new ArrayList<Constant>();
-				constantList.addAll(constants);
-				
-				constantList.sort((o1, o2) -> o1.name().compareToIgnoreCase(o2.name()));
-
-				
-				for (Constant c : constantList) {
-					if (c.value() >= value) {
-						rightConstantsComboBox.addItem(c.name());
-					}
-				}
-
-				if(rightConstantsComboBox.getItemCount() == 0){
-					rightUseConstant.setEnabled(false);
-				} else {
-					rightUseConstant.setEnabled(true);
-				}
-
-				if (oldRight != null)
-					rightConstantsComboBox.setSelectedItem(oldRight);
+        rightConstantsComboBox.removeAllItems();
+        Collection<Constant> constants = CreateGui.getCurrentTab().network()
+        .constants();
+
+        //List <Constant> constantList = new ArrayList(constants);
+        List <Constant> constantList = new ArrayList<Constant>();
+        constantList.addAll(constants);
+
+        constantList.sort((o1, o2) -> o1.name().compareToIgnoreCase(o2.name()));
+
+
+        for (Constant c : constantList) {
+            if (c.value() >= value) {
+                rightConstantsComboBox.addItem(c.name());
+            }
+        }
+
+        if(rightConstantsComboBox.getItemCount() == 0){
+            rightUseConstant.setEnabled(false);
+            rightUseConstant.setSelected(false);
+            updateRightComponents();
+        } else {
+            rightUseConstant.setEnabled(true);
+        }
+
+        if (oldRight != null)
+            rightConstantsComboBox.setSelectedItem(oldRight);
 	}
 
 	private void firstSpinnerStateChanged(ChangeEvent evt) {