jack.plugin.compile
Class VerifySourceAction

java.lang.Object
  extended byjack.plugin.compile.VerifySourceAction
All Implemented Interfaces:
org.eclipse.ui.IActionDelegate, org.eclipse.ui.IObjectActionDelegate

public class VerifySourceAction
extends java.lang.Object
implements org.eclipse.ui.IObjectActionDelegate

Popup action that allows to generate .jpo files when a java file is selected.

Author:
A. Requet, L. Burdy

Constructor Summary
VerifySourceAction()
          Constructor for Action1.
 
Method Summary
 void run(org.eclipse.jface.action.IAction action)
          Generates Proof Obligations 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

VerifySourceAction

public VerifySourceAction()
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 Proof Obligations 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)