Merge branch 'develop' into rodin3

de.prob.core/src/de/prob/eventb/translator/ContextTranslator.java

@@ -13,6 +13,7 @@ import java.util.LinkedList;
 import java.util.List;
 import java.util.Map;
 
+import org.apache.commons.lang.StringUtils;
 import org.eclipse.core.runtime.Assert;
 import org.eclipse.core.runtime.CoreException;
 import org.eventb.core.IContextRoot;
@@ -62,6 +63,7 @@ import de.prob.core.translator.TranslationFailedException;
 import de.prob.eventb.translator.internal.EProofStatus;
 import de.prob.eventb.translator.internal.ProofObligation;
 import de.prob.eventb.translator.internal.SequentSource;
+import de.prob.logging.Logger;
 
 public final class ContextTranslator extends AbstractComponentTranslator {
 
@@ -181,12 +183,12 @@ public final class ContextTranslator extends AbstractComponentTranslator {
 	}
 
 	private void collectProofInfo(IEventBRoot origin) throws RodinDBException {
+		List<String> bugs = new LinkedList<String>();
 
+		try {
 			IPSRoot proofStatus = origin.getPSRoot();
 			IPSStatus[] statuses = proofStatus.getStatuses();
 
-		List<String> bugs = new LinkedList<String>();
-
 			for (IPSStatus status : statuses) {
 				final int confidence = status.getConfidence();
 				boolean broken = status.isBroken();
@@ -222,6 +224,16 @@ public final class ContextTranslator extends AbstractComponentTranslator {
 				}
 				addProof(new ProofObligation(origin, s, name, pstatus));
 			}
+		} catch (RodinDBException e) {
+			bugs.add(e.getLocalizedMessage());
+		}
+		
+		if (!bugs.isEmpty()) {
+			String message = "Translation incomplete due to a Bug in Rodin. This does not affect correctness of the Animation/Model Checking but can decrease its performance. Skipped discharged information about: "
+					+ StringUtils.join(bugs, ",");
+			Logger.notifyUser(message);
+		}
+
 
 	}
 

de.prob.core/src/de/prob/eventb/translator/internal/ModelTranslator.java

@@ -171,13 +171,12 @@ public class ModelTranslator extends AbstractComponentTranslator {
 		addUnitPragmas(machine.getSCVariables());
 	}
 
-	private void collectProofInfo() throws RodinDBException {
-
+	private void collectProofInfo() {
+		List<String> bugs = new LinkedList<String>();
+		try {
 			IPSRoot proofStatus = machine.getPSRoot();
 			IPSStatus[] statuses = proofStatus.getStatuses();
 
-		List<String> bugs = new LinkedList<String>();
-
 			for (IPSStatus status : statuses) {
 				final int confidence = status.getConfidence();
 				boolean broken = status.isBroken();
@@ -221,6 +220,9 @@ public class ModelTranslator extends AbstractComponentTranslator {
 				}
 				addProof(new ProofObligation(origin, s, name, pstatus));
 			}
+		} catch (Exception e) {
+			bugs.add(e.getLocalizedMessage());
+		}
 
 		if (!bugs.isEmpty()) {
 			String message = "Translation incomplete due to a Bug in Rodin. This does not affect correctness of the Animation/Model Checking but can decrease its performance. Skipped discharged information about: "