diff --git a/de.prob.core/src/de/prob/core/command/AnalyseInvariantCommand.java b/de.prob.core/src/de/prob/core/command/AnalyseInvariantCommand.java deleted file mode 100644 index b5791a4c4efb21dbc3575f313fc9c082c78e3cf4..0000000000000000000000000000000000000000 --- a/de.prob.core/src/de/prob/core/command/AnalyseInvariantCommand.java +++ /dev/null @@ -1,48 +0,0 @@ -package de.prob.core.command; - -import de.prob.parser.ISimplifiedROMap; -import de.prob.prolog.output.IPrologTermOutput; -import de.prob.prolog.term.ListPrologTerm; -import de.prob.prolog.term.PrologTerm; - -public class AnalyseInvariantCommand implements ISimpleTextCommand { - - private static final String UNKNOWN = "Unknown"; - private static final String FALSE = "False"; - private static final String TOTAL = "Total"; - private static final String RESULT = "Result"; - private static final String DESCRIPTION = "Desc"; - private StringBuffer text; - - @Override - public void writeCommand(IPrologTermOutput pto) { - // analyse_predicate(Type,Desc,Result,Total,False,Unknown) - pto.openTerm("analyse_predicate").printAtom("invariant") - .printVariable(DESCRIPTION).printVariable(RESULT) - .printVariable(TOTAL).printVariable(FALSE) - .printVariable(UNKNOWN).closeTerm(); - } - - @Override - public void processResult(ISimplifiedROMap<String, PrologTerm> bindings) - throws CommandException { - text = new StringBuffer(); - text.append("Analysed: " + bindings.get(DESCRIPTION) + "\n"); - text.append("-------------------------------------\n"); - ListPrologTerm r = (ListPrologTerm) bindings.get(RESULT); - for (PrologTerm term : r) { - text.append(term); - text.append('\n'); - } - text.append("-------------------------------------\n"); - text.append("Total: " + bindings.get(TOTAL)+ "\n"); - text.append("False: " + bindings.get(FALSE)+ "\n"); - text.append("Unknown: " + bindings.get(UNKNOWN)); - } - - @Override - public String getResultingText() { - return text.toString(); - } - -} diff --git a/de.prob.core/src/de/prob/core/command/ISimpleTextCommand.java b/de.prob.core/src/de/prob/core/command/ISimpleTextCommand.java deleted file mode 100644 index 4abbfc3687137118c7ce4b23c7bb8bba54ea035e..0000000000000000000000000000000000000000 --- a/de.prob.core/src/de/prob/core/command/ISimpleTextCommand.java +++ /dev/null @@ -1,5 +0,0 @@ -package de.prob.core.command; - -public interface ISimpleTextCommand extends IComposableCommand{ - String getResultingText(); -} diff --git a/de.prob.plugin/fragment.xml b/de.prob.plugin/fragment.xml index 5a34b3033081a43252e1675ae80c7f0e0900d9f8..003705c9b993847e682ff7238824c32cc510ab92 100644 --- a/de.prob.plugin/fragment.xml +++ b/de.prob.plugin/fragment.xml @@ -30,13 +30,6 @@ name="contact"> </separator> </menu> - <menu - id="analyze" - label="Analyze"> - <separator - name="analyze"> - </separator> - </menu> </menu> </menuContribution> <menuContribution diff --git a/de.prob.ui/plugin.xml b/de.prob.ui/plugin.xml index 19428acddec4b510d4274d03eba54bd8d0bbfda6..13597907d5d7e2a7cd1560f639587afefcf03ef0 100644 --- a/de.prob.ui/plugin.xml +++ b/de.prob.ui/plugin.xml @@ -320,11 +320,6 @@ id="de.prob.ui.opview.checks" name="Checks"> </command> - <command - categoryId="de.prob.ui.commands.category" - id="de.prob.ui.exampleanalyzecommand" - name="Example for Analyze Commands"> - </command> <!-- <command id="de.prob.ui.startdmc" name="Start Distributed Modelcheck"> @@ -678,12 +673,6 @@ </enabledWhen> </handler> - <handler - commandId="de.prob.ui.exampleanalyzecommand"> - <class - class="de.prob.ui.internal.InvariantAnalyzeHandler"> - </class> - </handler> <handler commandId="de.prob.ui.ltl.counterexampleviewmenuhandler"> <class class="de.prob.ui.ltl.handler.CounterExampleViewMenuHandler"/> <enabledWhen> @@ -1194,18 +1183,6 @@ </command> </menu> </menuContribution> - <!-- - <menuContribution - allPopups="false" - locationURI="menu:analyze"> - <command - commandId="de.prob.ui.exampleanalyzecommand" - label="Analyze Invariant" - mnemonic="I" - style="toggle"> - </command> - </menuContribution> - --> <menuContribution locationURI="menu:de.prob.ui.ltl.CounterExampleView"> <menu label="Show as"> diff --git a/de.prob.ui/src/de/prob/ui/internal/GenericAnalyzeHandler.java b/de.prob.ui/src/de/prob/ui/internal/GenericAnalyzeHandler.java deleted file mode 100644 index 41168305cac6fff9a91c9aee50451abcbfe66f7c..0000000000000000000000000000000000000000 --- a/de.prob.ui/src/de/prob/ui/internal/GenericAnalyzeHandler.java +++ /dev/null @@ -1,113 +0,0 @@ -package de.prob.ui.internal; - -import org.eclipse.core.commands.AbstractHandler; -import org.eclipse.core.commands.ExecutionEvent; -import org.eclipse.core.commands.ExecutionException; -import org.eclipse.jface.dialogs.TitleAreaDialog; -import org.eclipse.swt.SWT; -import org.eclipse.swt.layout.GridData; -import org.eclipse.swt.widgets.Composite; -import org.eclipse.swt.widgets.Control; -import org.eclipse.swt.widgets.Shell; -import org.eclipse.swt.widgets.Text; -import org.eclipse.ui.handlers.HandlerUtil; - -import de.prob.core.Animator; -import de.prob.core.ProBCommandJob; -import de.prob.core.ProBJobFinishedListener; -import de.prob.core.command.CommandException; -import de.prob.core.command.IComposableCommand; -import de.prob.core.command.ISimpleTextCommand; -import de.prob.logging.Logger; - -public abstract class GenericAnalyzeHandler extends AbstractHandler { - - public class GenericAnalyzeFinishedHandler extends ProBJobFinishedListener { - - private final Shell shell; - - public GenericAnalyzeFinishedHandler(Shell shell) { - this.shell = shell; - } - - @Override - protected void showResult(IComposableCommand command, Animator animator) { - if (command instanceof ISimpleTextCommand) { - ISimpleTextCommand textcommand = (ISimpleTextCommand) command; - String text = textcommand.getResultingText(); - display(text); - } else { - Logger.notifyUser( - "The invoked command did not implement the correct interface. Please report this bug.", - new CommandException( - "Error in " - + command.getClass() - + ". Class should implement ISimpleTextCommand.")); - } - } - - private void display(final String text) { - - final TitleAreaDialog titleAreaDialog = new TitleAreaDialog(shell) { - - @Override - protected Control createDialogArea(Composite parent) { - - setTitle(name); - - Composite composite = (Composite) super - .createDialogArea(parent); - Text t = new Text(composite, SWT.WRAP | SWT.MULTI | SWT.BORDER - | SWT.H_SCROLL | SWT.V_SCROLL); - GridData gridData = - new GridData( - GridData.HORIZONTAL_ALIGN_FILL | GridData.VERTICAL_ALIGN_FILL); - gridData.grabExcessVerticalSpace = true; - - t.setLayoutData(gridData); - - - t.append(text); - return composite; - } - - }; - - final Runnable runnable = new Runnable() { - @Override - public void run() { - titleAreaDialog.open(); - } - }; - shell.getDisplay().asyncExec(runnable); - } - } - - private final ISimpleTextCommand command; - private final String name; - - public GenericAnalyzeHandler(ISimpleTextCommand command, String name) { - this.command = command; - this.name = name; - } - - @Override - public Object execute(ExecutionEvent event) throws ExecutionException { - final Shell shell = HandlerUtil.getActiveShell(event); - Animator animator = Animator.getAnimator(); - if (animator.isMachineLoaded()) { - final ProBCommandJob job = new ProBCommandJob(name, animator, - command); - GenericAnalyzeFinishedHandler finishedHandler = new GenericAnalyzeFinishedHandler( - shell); - job.setUser(true); - job.addJobChangeListener(finishedHandler); - job.schedule(); - - } else { - Logger.notifyUser("No ProB animation running. This is a bug. Please submit a report. Error in declaraion of class "+this.getClass()); - } - return null; - } - -} diff --git a/de.prob.ui/src/de/prob/ui/internal/InvariantAnalyzeHandler.java b/de.prob.ui/src/de/prob/ui/internal/InvariantAnalyzeHandler.java deleted file mode 100644 index e7001d44c1b35e59b25664f1891b03a410659a75..0000000000000000000000000000000000000000 --- a/de.prob.ui/src/de/prob/ui/internal/InvariantAnalyzeHandler.java +++ /dev/null @@ -1,11 +0,0 @@ -package de.prob.ui.internal; - -import de.prob.core.command.AnalyseInvariantCommand; - -public class InvariantAnalyzeHandler extends GenericAnalyzeHandler { - - public InvariantAnalyzeHandler() { - super(new AnalyseInvariantCommand(), "Analyze Invariant"); - } - -}