Merge branch 'develop' of github.com:bendisposto/prob into develop

README.md

@@ -13,28 +13,23 @@ The ProB binary and source distributions contain the nauty library (http://cs.an
 
 For availability of commercial support, please contact Formal Mind (http://www.formalmind.com).
 
-# Contributing
-
-## Setting up the development environment
+# Setting up the development environment
 
 - Clone the repository (http://github.com/bendisposto/prob) 
   We suggest to fork the project on github (see https://help.github.com/articles/fork-a-repo)
 
-- We use gradle to manage the dependencies to the libraries, so you will need gradle installed on your computer. 
+- We use gradle to manage the dependencies to the libraries, thus you will need gradle installed on your computer. 
   (see http://www.gradle.org/)
 
-- Open a shell and cd into the de.prob.releng directory
-
-- Run the downloadCli task (gradle downloadCli). This will download the latest nightly build of the Prolog binary.
-
-- Run the collectDependencies task (gradle collectDependencies). This will download the required libraries (such as apache commons, etc.)
+- In the de.prob.releng directory run the downloadCli and collectDependencies tasks (gradle downloadCli collectDependencies). This will download the latest nightly build of the Prolog binary and the required Java libraries (such as apache commons, etc.)
 
 - Install Eclipse (Indigo/Juno) for RCP Development
 
-- Import the projects into Eclipse (note that de.prob.releng is not an Eclipse project, it can be left out). At this point Eclipse will show many errors, the reason is that the Target platform (i.e., Rodin hasn't been setup yet)
+- Import the projects into Eclipse. You can leave out de.prob.releng.  At this point Eclipse will complain about errors, the reason is that the target platform (i.e., Rodin) hasn't been setup yet).
 
 - Open the file prob_target.target from the de.prob.core project and click on "Set as Target Platform". Grab a coffee. 
 
+- After the target platform was installed and the workspace has been compiled you can run the project as an Eclipse application (use org.rodinp.platform.product as the product in the run configuration)
 
 
 

de.prob.core/build.properties

@@ -4,15 +4,6 @@ bin.includes = META-INF/,\
                plugin.xml,\
                .,\
                prob/,\
-               lib/dependencies,\
-               lib/dependencies/answerparser-2.4.8-SNAPSHOT.jar,\
-               lib/dependencies/bparser-2.4.8-SNAPSHOT.jar,\
-               lib/dependencies/cliparser-2.4.8-SNAPSHOT.jar,\
-               lib/dependencies/commons-lang-2.6.jar,\
-               lib/dependencies/jgrapht-0.8.3.jar,\
-               lib/dependencies/jsr305-1.3.9.jar,\
-               lib/dependencies/ltlparser-2.4.8-SNAPSHOT.jar,\
-               lib/dependencies/parserbase-2.4.8-SNAPSHOT.jar,\
-               lib/dependencies/prologlib-2.4.8-SNAPSHOT.jar,\
-               lib/dependencies/unicode-2.4.8-SNAPSHOT.jar
+               lib/
+             
 

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

@@ -8,7 +8,6 @@ package de.prob.eventb.translator; // NOPMD
 // High number of imports because it depends on AST
 
 import java.util.ArrayList;
-import java.util.Collections;
 import java.util.LinkedList;
 import java.util.List;
 
@@ -26,7 +25,6 @@ import org.eventb.core.ast.RelationalPredicate;
 import org.eventb.core.ast.SimplePredicate;
 import org.eventb.core.ast.UnaryPredicate;
 
-import de.be4.classicalb.core.parser.analysis.pragma.internal.ClassifiedPragma;
 import de.be4.classicalb.core.parser.node.AConjunctPredicate;
 import de.be4.classicalb.core.parser.node.ADisjunctPredicate;
 import de.be4.classicalb.core.parser.node.AEqualPredicate;
@@ -52,7 +50,6 @@ import de.be4.classicalb.core.parser.node.ASubsetStrictPredicate;
 import de.be4.classicalb.core.parser.node.ATruthPredicate;
 import de.be4.classicalb.core.parser.node.PExpression;
 import de.be4.classicalb.core.parser.node.PPredicate;
-import de.hhu.stups.sablecc.patch.SourcePosition;
 import de.prob.eventb.translator.internal.SimpleVisitorAdapter;
 
 public class PredicateVisitor extends SimpleVisitorAdapter implements // NOPMD

de.prob.core/src/de/prob/eventb/translator2/EMFEventBTranslator.java

@@ -9,7 +9,6 @@ import org.eclipse.emf.common.util.EList;
 import org.eventb.core.IEventBRoot;
 import org.eventb.emf.core.EventBNamedCommentedComponentElement;
 import org.eventb.emf.core.Project;
-import org.eventb.emf.core.context.Axiom;
 import org.eventb.emf.core.context.CarrierSet;
 import org.eventb.emf.core.context.Context;
 import org.eventb.emf.core.machine.Machine;
@@ -55,10 +54,6 @@ public class EMFEventBTranslator {
 			setList.add(deferredSet);
 		}
 
-		EList<Axiom> axioms = c.getAxioms();
-		
-		
-
 	}
 
 	public void printMachine(IPrologTermOutput pto, Machine m) {

de.prob.core/src/de/prob/logging/Logger.java

@@ -78,7 +78,8 @@ public final class Logger {
 	/**
 	 * Check a property. The method notifies the user and throws an exception if
 	 * the assertion fails. <br>
-	 * <b>Examples:</b><br>{@code Logger.assertProB(this.getClass(),"x != null", x
+	 * <b>Examples:</b><br>
+	 * {@code Logger.assertProB(this.getClass(),"x != null", x
 	 * != null); } <br>
 	 * {@code Logger.assertProB(this.getClass(),"x should not be null", x != null); }
 	 * <br>
@@ -112,7 +113,8 @@ public final class Logger {
 
 	/**
 	 * Failed assertion. The method notifies the user and throws an exception. <br>
-	 * <b>Examples:</b><br>{@code if (!file.exists()) String message =
+	 * <b>Examples:</b><br>
+	 * {@code if (!file.exists()) String message =
 	 * "Called open on nonexisting file " + file;
 	 * Logger.assertProB(EditorPlugin.class, message); }
 	 * 
@@ -149,4 +151,8 @@ public final class Logger {
 	private static void log(final IStatus status) {
 		Activator.getDefault().getLog().log(status);
 	}
+
+	public static void notifyUserAboutWarningWithoutBugreport(String string) {
+		log(IStatus.WARNING, NOBUGREPORT, string, null);
+	}
 }

de.prob.ui/src/de/prob/ui/eventb/StartAnimationHandler.java

 package de.prob.ui.eventb;
 
+import java.util.ArrayList;
+import java.util.List;
+
 import org.eclipse.core.commands.AbstractHandler;
 import org.eclipse.core.commands.ExecutionEvent;
 import org.eclipse.core.commands.ExecutionException;
@@ -67,9 +70,22 @@ public class StartAnimationHandler extends AbstractHandler implements IHandler {
 		final IEventBRoot rootElement = getRootElement();
 		final IFile resource = extractResource(rootElement);
 
-		if (!checkErrorMarkers(resource)) {
-			String message = "A model/context in your project contains Errors or Warnings. This can lead to unexpected behavior (e.g. missing variables) when animating.";
-			Logger.notifyUserWithoutBugreport(message);
+		ArrayList<String> errors = new ArrayList<String>();
+		boolean realError = checkErrorMarkers(resource, errors);
+		if (!errors.isEmpty()) {
+			String message = "Some components in your project contain "
+					+ (realError ? "errors" : "warnings")
+					+ ". This can lead to unexpected behavior (e.g. missing variables) when animating.\n\nDetails:\n";
+			StringBuffer stringBuffer = new StringBuffer(message);
+			for (String string : errors) {
+				stringBuffer.append(string);
+				stringBuffer.append('\n');
+			}
+			if (realError)
+				Logger.notifyUserWithoutBugreport(stringBuffer.toString());
+			else
+				Logger.notifyUserAboutWarningWithoutBugreport(stringBuffer
+						.toString());
 		}
 		;
 
@@ -90,17 +106,25 @@ public class StartAnimationHandler extends AbstractHandler implements IHandler {
 		return null;
 	}
 
-	private boolean checkErrorMarkers(final IFile resource) {
+	private boolean checkErrorMarkers(final IFile resource, List<String> errors) {
+		boolean result = false;
 		IProject project = resource.getProject();
 		try {
 			IMarker[] markers = project.findMarkers(
 					"org.eclipse.core.resources.problemmarker", true,
 					IResource.DEPTH_INFINITE);
-			return markers.length == 0;
-		} catch (CoreException e1) {
+			for (IMarker iMarker : markers) {
+				errors.add(iMarker.getResource().getName()
+						+ ": "
+						+ iMarker
+								.getAttribute(IMarker.MESSAGE, "unknown Error"));
+				result = result
+						|| (Integer) iMarker.getAttribute(IMarker.SEVERITY) == IMarker.SEVERITY_ERROR;
+			}
 
+		} catch (CoreException e1) {
 		}
-		return false;
+		return result;
 	}
 
 	private IEventBRoot getRootElement() {

de.prob.ui/src/de/prob/ui/ticket/ProBLogListener.java

@@ -30,12 +30,13 @@ public final class ProBLogListener implements ILogListener {
 			final boolean bugreport = false; // ;code == Logger.BUGREPORT;
 			display.asyncExec(new Runnable() {
 				public void run() {
+					String title = (status.getSeverity() == IStatus.ERROR) ? "An Error occured"
+							: "Warning";
 					// Notice: ErrorTICKETDialog to provide Bugreport-Button
 					ErrorTicketDialog.openError(display.getActiveShell(),
-							"Error", "An error occured.", status, bugreport);
+							"ProB Problem", title, status, bugreport);
 				}
-			}
-			);
+			});
 		}
 
 		display.asyncExec(new Runnable() {