diff --git a/de.bmotionstudio.gef.editor/src/de/bmotionstudio/gef/editor/eventb/EventBHelper.java b/de.bmotionstudio.gef.editor/src/de/bmotionstudio/gef/editor/eventb/EventBHelper.java index 4fd4504a7ddb5e6a299050aa56703ae0875b9e47..62f1087c4a17fafe0483af6149f0ac8ccf909ee4 100644 --- a/de.bmotionstudio.gef.editor/src/de/bmotionstudio/gef/editor/eventb/EventBHelper.java +++ b/de.bmotionstudio.gef.editor/src/de/bmotionstudio/gef/editor/eventb/EventBHelper.java @@ -39,13 +39,13 @@ public final class EventBHelper { public static EventBRoot getCorrespondingFile(IFile file, String machineFileName) { IRodinProject rProject = RodinCore.valueOf(file.getProject()); - EventBRoot machineRoot = null; + EventBRoot root = null; if (rProject != null) { IRodinFile rFile = rProject.getRodinFile(machineFileName); if (rFile != null && rFile.getRoot() instanceof EventBRoot) - machineRoot = (EventBRoot) rFile.getRoot(); + root = (EventBRoot) rFile.getRoot(); } - return machineRoot; + return root; } public static List<MachineOperation> getOperations( @@ -58,9 +58,12 @@ public final class EventBHelper { EventBRoot correspondingFile = getCorrespondingFile( visualization.getProjectFile(), visualization.getMachineName()); - ISCMachineRoot machineRoot = correspondingFile.getSCMachineRoot(); - if (machineRoot != null) { + if (correspondingFile instanceof MachineRoot + && correspondingFile.exists()) { + + ISCMachineRoot machineRoot = correspondingFile + .getSCMachineRoot(); try { @@ -91,10 +94,10 @@ public final class EventBHelper { .unmodifiableList(new ArrayList<MachineOperation>()); } + } else if (visualization.getLanguage().equals("ClassicalB")) { + // TODO: Implement me!!! } - } else if (visualization.getLanguage().equals("ClassicalB")) { - // TODO: Implement me!!! } return tmpSet; @@ -106,28 +109,30 @@ public final class EventBHelper { EventBRoot correspondingFile = getCorrespondingFile( visualization.getProjectFile(), visualization.getMachineName()); - ISCMachineRoot machineRoot = correspondingFile.getSCMachineRoot(); - ISCVariable[] vars = null; ArrayList<MachineContentObject> tmpSet = new ArrayList<MachineContentObject>(); - try { - vars = machineRoot.getSCVariables(); + if (correspondingFile instanceof MachineRoot + && correspondingFile.exists()) { - for (ISCVariable var : vars) { - - MachineContentObject machinevar = new MachineContentObject( - var.getIdentifierString()); - machinevar.setType(var.getType(formularFactory)); - tmpSet.add(machinevar); + ISCMachineRoot machineRoot = correspondingFile.getSCMachineRoot(); + try { + ISCVariable[] vars = machineRoot.getSCVariables(); + for (ISCVariable var : vars) { + MachineContentObject machinevar = new MachineContentObject( + var.getIdentifierString()); + machinevar.setType(var.getType(formularFactory)); + tmpSet.add(machinevar); + } + } catch (RodinDBException e) { + String message = "Rodin DB Exception while getting variables: " + + e.getLocalizedMessage(); + Logger.notifyUser(message, e); + return Collections + .unmodifiableList(new ArrayList<MachineContentObject>()); } - } catch (RodinDBException e) { - String message = "Rodin DB Exception while getting variables: " - + e.getLocalizedMessage(); - Logger.notifyUser(message, e); - return Collections - .unmodifiableList(new ArrayList<MachineContentObject>()); + } return tmpSet; @@ -138,32 +143,34 @@ public final class EventBHelper { Visualization visualization) { EventBRoot correspondingFile = getCorrespondingFile( - visualization.getProjectFile(), - visualization.getMachineName()); - ISCMachineRoot machineRoot = correspondingFile.getSCMachineRoot(); + visualization.getProjectFile(), visualization.getMachineName()); - ISCInvariant[] invariants = null; ArrayList<MachineContentObject> tmpSet = new ArrayList<MachineContentObject>(); - try { - invariants = machineRoot.getSCInvariants(); - - for (ISCInvariant inv : invariants) { + if (correspondingFile instanceof MachineRoot + && correspondingFile.exists()) { - MachineContentObject machineinv = new MachineContentObject( - inv.getPredicateString()); - tmpSet.add(machineinv); + ISCMachineRoot machineRoot = correspondingFile.getSCMachineRoot(); + try { + ISCInvariant[] invariants = machineRoot.getSCInvariants(); + for (ISCInvariant inv : invariants) { + MachineContentObject machineinv = new MachineContentObject( + inv.getPredicateString()); + tmpSet.add(machineinv); + } + } catch (RodinDBException e) { + String message = "Rodin DB Exception while getting invariants: " + + e.getLocalizedMessage(); + Logger.notifyUser(message, e); + return Collections + .unmodifiableList(new ArrayList<MachineContentObject>()); } - } catch (RodinDBException e) { - String message = "Rodin DB Exception while getting invariants: " - + e.getLocalizedMessage(); - Logger.notifyUser(message, e); - return Collections - .unmodifiableList(new ArrayList<MachineContentObject>()); + } return tmpSet; + } public static List<MachineContentObject> getConstants( @@ -173,46 +180,52 @@ public final class EventBHelper { visualization.getProjectFile(), visualization.getMachineName()); ArrayList<MachineContentObject> tmpSet = new ArrayList<MachineContentObject>(); - try { - if (correspondingFile instanceof MachineRoot) { - ISCMachineRoot machineRoot = correspondingFile - .getSCMachineRoot(); + if (correspondingFile.exists()) { + + try { + if (correspondingFile instanceof MachineRoot) { + + ISCMachineRoot machineRoot = correspondingFile + .getSCMachineRoot(); - ISCInternalContext[] seenContexts = machineRoot - .getSCSeenContexts(); - for (ISCInternalContext context : seenContexts) { + ISCInternalContext[] seenContexts = machineRoot + .getSCSeenContexts(); + for (ISCInternalContext context : seenContexts) { - for (ISCConstant constant : context.getSCConstants()) { + for (ISCConstant constant : context.getSCConstants()) { + + MachineContentObject machineinv = new MachineContentObject( + constant.getIdentifierString()); + machineinv.setType(constant + .getType(formularFactory)); + tmpSet.add(machineinv); + + } + + } + } else if (correspondingFile instanceof ContextRoot) { + + ISCContextRoot contextRoot = correspondingFile + .getSCContextRoot(); + for (ISCConstant constant : contextRoot.getSCConstants()) { MachineContentObject machineinv = new MachineContentObject( constant.getIdentifierString()); machineinv.setType(constant.getType(formularFactory)); tmpSet.add(machineinv); - } } - } else if (correspondingFile instanceof ContextRoot) { - - ISCContextRoot contextRoot = correspondingFile - .getSCContextRoot(); - for (ISCConstant constant : contextRoot.getSCConstants()) { - MachineContentObject machineinv = new MachineContentObject( - constant.getIdentifierString()); - machineinv.setType(constant.getType(formularFactory)); - tmpSet.add(machineinv); - } - + } catch (RodinDBException e) { + String message = "Rodin DB Exception while getting constants: " + + e.getLocalizedMessage(); + Logger.notifyUser(message, e); + return Collections + .unmodifiableList(new ArrayList<MachineContentObject>()); } - } catch (RodinDBException e) { - String message = "Rodin DB Exception while getting constants: " - + e.getLocalizedMessage(); - Logger.notifyUser(message, e); - return Collections - .unmodifiableList(new ArrayList<MachineContentObject>()); } return tmpSet; diff --git a/de.bmotionstudio.gef.editor/src/de/bmotionstudio/gef/editor/observer/TableObserver.java b/de.bmotionstudio.gef.editor/src/de/bmotionstudio/gef/editor/observer/TableObserver.java index cee21033f1ceb5fcd6effd76e383e9346aff14a3..c872dec8943a50784c163d98d53c3d548c32d875 100644 --- a/de.bmotionstudio.gef.editor/src/de/bmotionstudio/gef/editor/observer/TableObserver.java +++ b/de.bmotionstudio.gef.editor/src/de/bmotionstudio/gef/editor/observer/TableObserver.java @@ -15,6 +15,8 @@ public class TableObserver extends Observer { private String expression; private String predicate; + private boolean overrideCells; + private boolean keepHeader; public static List<String> split(String input, char tempReplacement) { while (input.matches(".*\\{[^\\}]+,[^\\}]+\\}.*")) { @@ -60,21 +62,24 @@ public class TableObserver extends Observer { fEval = fEval.replaceAll("^\\{", ""); fEval = fEval.replaceAll("\\}$", ""); - // System.out.println(fEval); - - // String input = "aa, a, aa, {bb, 1, 2}, {cc}, {dd,5}"; String input = fEval; List<String> rows = split(input, '#'); - AbstractAttribute attributeRows = control - .getAttribute(AttributeConstants.ATTRIBUTE_ROWS); - Integer numberOfOldRows = Integer.valueOf(attributeRows - .getInitValue().toString()); - - AbstractAttribute attributeColumns = control - .getAttribute(AttributeConstants.ATTRIBUTE_COLUMNS); - Integer numberOfOldColumns = Integer.valueOf(attributeColumns - .getInitValue().toString()); + Integer numberOfOldRows = 0; + Integer numberOfOldColumns = 0; + + if (!overrideCells) { + AbstractAttribute attributeRows = control + .getAttribute(AttributeConstants.ATTRIBUTE_ROWS); + numberOfOldRows = Integer.valueOf(attributeRows.getInitValue() + .toString()); + AbstractAttribute attributeColumns = control + .getAttribute(AttributeConstants.ATTRIBUTE_COLUMNS); + numberOfOldColumns = Integer.valueOf(attributeColumns + .getInitValue().toString()); + } else if (keepHeader) { + numberOfOldRows = 1; + } int numberOfNewRows = rows.size(); @@ -123,14 +128,6 @@ public class TableObserver extends Observer { } - // private Iterable<MatchResult> findMatches(String pattern, CharSequence s) - // { - // List<MatchResult> results = new ArrayList<MatchResult>(); - // for (Matcher m = Pattern.compile(pattern).matcher(s); m.find();) - // results.add(m.toMatchResult()); - // return results; - // } - public void setExpression(String expression) { this.expression = expression; } @@ -152,4 +149,20 @@ public class TableObserver extends Observer { return new WizardTableObserver(control, this); } + public boolean isOverrideCells() { + return overrideCells; + } + + public void setOverrideCells(boolean overrideCells) { + this.overrideCells = overrideCells; + } + + public boolean isKeepHeader() { + return keepHeader; + } + + public void setKeepHeader(boolean keepHeader) { + this.keepHeader = keepHeader; + } + } diff --git a/de.bmotionstudio.gef.editor/src/de/bmotionstudio/gef/editor/observer/wizard/WizardTableObserver.java b/de.bmotionstudio.gef.editor/src/de/bmotionstudio/gef/editor/observer/wizard/WizardTableObserver.java index 6d5a7a66c6e363515add29d40d4153d00a92273c..9e6ef3952c7faae6911fae423ef390701eb8980f 100644 --- a/de.bmotionstudio.gef.editor/src/de/bmotionstudio/gef/editor/observer/wizard/WizardTableObserver.java +++ b/de.bmotionstudio.gef.editor/src/de/bmotionstudio/gef/editor/observer/wizard/WizardTableObserver.java @@ -21,13 +21,14 @@ import org.eclipse.swt.graphics.FontData; import org.eclipse.swt.graphics.Point; import org.eclipse.swt.layout.GridData; import org.eclipse.swt.layout.GridLayout; +import org.eclipse.swt.layout.RowLayout; +import org.eclipse.swt.widgets.Button; import org.eclipse.swt.widgets.Composite; import org.eclipse.swt.widgets.Display; +import org.eclipse.swt.widgets.Group; import org.eclipse.swt.widgets.Label; import org.eclipse.swt.widgets.List; import org.eclipse.swt.widgets.Text; -import org.eventb.core.ast.Expression; -import org.eventb.core.ast.FormulaFactory; import org.eventb.core.ast.PowerSetType; import de.bmotionstudio.gef.editor.eventb.EventBHelper; @@ -36,7 +37,6 @@ import de.bmotionstudio.gef.editor.model.BControl; import de.bmotionstudio.gef.editor.observer.Observer; import de.bmotionstudio.gef.editor.observer.ObserverWizard; import de.bmotionstudio.gef.editor.observer.TableObserver; -import de.prob.unicode.UnicodeTranslator; public class WizardTableObserver extends ObserverWizard { @@ -44,6 +44,8 @@ public class WizardTableObserver extends ObserverWizard { private Text txtExpression; private Text txtPredicate; + private Button cbOverrideCells; + private Button cbKeepHeader; public Text getTxtExpression() { return txtExpression; @@ -57,8 +59,27 @@ public class WizardTableObserver extends ObserverWizard { final DataBindingContext dbc = new DataBindingContext(); - Composite container = new Composite(parent, SWT.NONE); + parent.setLayout(new GridLayout(1, true)); + + Group group = new Group(parent, SWT.None); + group.setText("General settings"); + RowLayout rowLayout = new RowLayout(); + rowLayout.marginLeft = 10; + rowLayout.marginTop = 10; + rowLayout.marginBottom = 10; + group.setLayout(rowLayout); + group.setLayoutData(new GridData(GridData.FILL_HORIZONTAL)); + + cbOverrideCells = new Button(group, SWT.CHECK); + cbOverrideCells.setText("Override cells"); + + cbKeepHeader = new Button(group, SWT.CHECK); + cbKeepHeader.setText("Keep header"); + + Group container = new Group(parent, SWT.None); + container.setText("Formal model"); container.setLayout(new GridLayout(2, false)); + container.setLayoutData(new GridData(GridData.FILL_BOTH)); Composite conLeft = new Composite(container, SWT.NONE); conLeft.setLayoutData(new GridData(GridData.FILL_BOTH)); @@ -94,10 +115,6 @@ public class WizardTableObserver extends ObserverWizard { .getConstants(getBControl().getVisualization()); for (MachineContentObject mobj : constants) { if (mobj.getType() instanceof PowerSetType) { - Expression expression = ((PowerSetType) mobj.getType()) - .toExpression(FormulaFactory.getDefault()); - System.out.println(UnicodeTranslator.toAscii(expression - .toString())); relationList.add(mobj.getLabel()); } } @@ -106,10 +123,6 @@ public class WizardTableObserver extends ObserverWizard { .getVariables(getBControl().getVisualization()); for (MachineContentObject mobj : variables) { if (mobj.getType() instanceof PowerSetType) { - Expression expression = ((PowerSetType) mobj.getType()) - .toExpression(FormulaFactory.getDefault()); - System.out.println(UnicodeTranslator.toAscii(expression - .toString())); relationList.add(mobj.getLabel()); } } @@ -143,6 +156,14 @@ public class WizardTableObserver extends ObserverWizard { BeansObservables.observeValue( (TableObserver) getObserver(), "expression")); + dbc.bindValue(SWTObservables.observeSelection(cbOverrideCells), + BeansObservables.observeValue( + (TableObserver) getObserver(), "overrideCells")); + + dbc.bindValue(SWTObservables.observeSelection(cbKeepHeader), + BeansObservables.observeValue( + (TableObserver) getObserver(), "keepHeader")); + } }