jack.plugin.source
Class AddJmlAction

java.lang.Object
  jack.plugin.source.AddJmlAction

All Implemented Interfaces:

org.eclipse.ui.IActionDelegate, org.eclipse.ui.IObjectActionDelegate

public class AddJmlAction

extends java.lang.Object

implements org.eclipse.ui.IObjectActionDelegate

Action allowing to generate JML specification.

Author:

L. Burdy

Constructor Summary

AddJmlAction()
Constructor for Action1.

Method Summary

void	run(org.eclipse.jface.action.IAction action) Generates JML specifications for the selected compilation units.
void	selectionChanged(org.eclipse.jface.action.IAction action, org.eclipse.jface.viewers.ISelection selection) Update the selection accordingly to the selection changes within the editor.
void	setActivePart(org.eclipse.jface.action.IAction action, org.eclipse.ui.IWorkbenchPart targetPart)

Methods inherited from class java.lang.Object

equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

AddJmlAction

public AddJmlAction()

Constructor for Action1.

Method Detail

setActivePart

public void setActivePart(org.eclipse.jface.action.IAction action,
                          org.eclipse.ui.IWorkbenchPart targetPart)

Specified by:

setActivePart in interface org.eclipse.ui.IObjectActionDelegate

Parameters:

action - the action proxy that handles presentation portion of the action

targetPart - the new part target

See Also:

Sets the active part for the delegate. The active part is commonly used to get a working context for the action, such as the shell for any dialog which is needed.

This method will be called every time the action appears in a popup menu. The targetPart may change with each invocation.

run

public void run(org.eclipse.jface.action.IAction action)

Generates JML specifications for the selected compilation units.

Specified by:

run in interface org.eclipse.ui.IActionDelegate

See Also:

IActionDelegate#run(IAction)

selectionChanged

public void selectionChanged(org.eclipse.jface.action.IAction action,
                             org.eclipse.jface.viewers.ISelection selection)

Update the selection accordingly to the selection changes within the editor.

Specified by:

selectionChanged in interface org.eclipse.ui.IActionDelegate

See Also:

IActionDelegate#selectionChanged(IAction, ISelection)