PROBPLUGIN: ProB Animate Menu for Shared Event Composed Machine

Description

The ProB “Animate” and “Export to Classical B” menu commands are available for Shared Event Composed machines.
However, neither command works for those files.
The Animate command throws an exception on the Console, but no feedback is given to the user.
(The “Export to classical B" command returns an error message to the user.)

Probably we should simply disable those commands for these types of files.

> java.lang.NullPointerException
> at de.prob.ui.eventb.StartAnimationHandler.checkErrorMarkers(StartAnimationHandler.java:114)
> at de.prob.ui.eventb.StartAnimationHandler.execute(StartAnimationHandler.java:77)
> at org.eclipse.ui.internal.handlers.HandlerProxy.execute(HandlerProxy.java:293)
> at org.eclipse.core.commands.Command.executeWithChecks(Command.java:476)
> at org.eclipse.core.commands.ParameterizedCommand.executeWithChecks(ParameterizedCommand.java:508)
> at org.eclipse.ui.internal.handlers.HandlerService.executeCommand(HandlerService.java:169)
> at org.eclipse.ui.internal.handlers.SlaveHandlerService.executeCommand(SlaveHandlerService.java:241)
> at org.eclipse.ui.internal.handlers.SlaveHandlerService.executeCommand(SlaveHandlerService.java:241)
> at org.eclipse.ui.menus.CommandContributionItem.handleWidgetSelection(CommandContributionItem.java:829)
> at org.eclipse.ui.menus.CommandContributionItem.access$19(CommandContributionItem.java:815)
> at org.eclipse.ui.menus.CommandContributionItem$5.handleEvent(CommandContributionItem.java:805)
> at org.eclipse.swt.widgets.EventTable.sendEvent(EventTable.java:84)
> at org.eclipse.swt.widgets.Display.sendEvent(Display.java:4128)
> at org.eclipse.swt.widgets.Widget.sendEvent(Widget.java:1457)
> at org.eclipse.swt.widgets.Widget.sendEvent(Widget.java:1480)
> at org.eclipse.swt.widgets.Widget.sendEvent(Widget.java:1465)
> at org.eclipse.swt.widgets.Widget.notifyListeners(Widget.java:1270)
> at org.eclipse.swt.widgets.Display.runDeferredEvents(Display.java:3974)
> at org.eclipse.swt.widgets.Display.readAndDispatch(Display.java:3613)
> at org.eclipse.ui.internal.Workbench.runEventLoop(Workbench.java:2701)
> at org.eclipse.ui.internal.Workbench.runUI(Workbench.java:2665)
> at org.eclipse.ui.internal.Workbench.access$4(Workbench.java:2499)
> at org.eclipse.ui.internal.Workbench$7.run(Workbench.java:679)
> at org.eclipse.core.databinding.observable.Realm.runWithDefault(Realm.java:332)
> at org.eclipse.ui.internal.Workbench.createAndRunWorkbench(Workbench.java:668)
> at org.eclipse.ui.PlatformUI.createAndRunWorkbench(PlatformUI.java:149)
> at org.eclipse.ui.internal.ide.application.IDEApplication.start(IDEApplication.java:123)
> at org.eclipse.equinox.internal.app.EclipseAppHandle.run(EclipseAppHandle.java:196)
> at org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.runApplication(EclipseAppLauncher.java:110)
> at org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.start(EclipseAppLauncher.java:79)
> at org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:344)
> at org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:179)
> at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
> at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:39)
> at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:25)
> at java.lang.reflect.Method.invoke(Method.java:597)
> at org.eclipse.equinox.launcher.Main.invokeFramework(Main.java:622)
> at org.eclipse.equinox.launcher.Main.basicRun(Main.java:577)
> at org.eclipse.equinox.launcher.Main.run(Main.java:1410)
>

Environment

None

Attachments

1

Gliffy Diagrams

Activity

Show:

Sebastian Krings January 30, 2014 at 10:06 AM

Buttons are now only shown on IMachineRoot and IContextRoot (i.e. not for Theories, Composed Machines, ....)

Fixed

Details

Assignee

Reporter

Priority

More fields

Created January 20, 2014 at 12:35 PM
Updated January 30, 2014 at 10:06 AM
Resolved January 30, 2014 at 10:06 AM