jack.plugin.edit
Class EditButton

java.lang.Object
  jack.plugin.ToolbarButton
      jack.plugin.edit.EditButton

All Implemented Interfaces:

org.eclipse.ui.IActionDelegate, org.eclipse.ui.IWorkbenchWindowActionDelegate

public class EditButton

extends ToolbarButton

Button allowing to "edit" the selected JML file.

If several JML files are selected, then one of them is chosen.

Author:

A. Requet, L. Burdy

Constructor Summary

EditButton()

Method Summary

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

Methods inherited from class jack.plugin.ToolbarButton

dispose, getSelection, getWindow, init, runProofTask, selectionChanged

Methods inherited from class java.lang.Object

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

Constructor Detail

EditButton

public EditButton()

Method Detail

run

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

See Also:

IActionDelegate.run(IAction)