org.jmlspecs.eclipse.jdt.ui.preferences
Class JmlConfigurationBlock

java.lang.Object
  org.eclipse.jdt.internal.ui.preferences.OptionsConfigurationBlock
      org.jmlspecs.eclipse.jdt.ui.preferences.JmlConfigurationBlock

public class JmlConfigurationBlock
extends org.eclipse.jdt.internal.ui.preferences.OptionsConfigurationBlock

Nested Class Summary

Nested classes/interfaces inherited from class org.eclipse.jdt.internal.ui.preferences.OptionsConfigurationBlock

org.eclipse.jdt.internal.ui.preferences.OptionsConfigurationBlock.Key

Constructor Summary

JmlConfigurationBlock(org.eclipse.jdt.internal.ui.wizards.IStatusChangeListener context, IProject project, org.eclipse.ui.preferences.IWorkbenchPreferenceContainer container)

Method Summary

void

dispose()

Methods inherited from class org.eclipse.jdt.internal.ui.preferences.OptionsConfigurationBlock

areSettingsEnabled, hasProjectSpecificOptions, performApply, performDefaults, performOk, performRevert, selectOption, selectOption, useProjectSpecificSettings

Methods inherited from class java.lang.Object

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

Constructor Detail

JmlConfigurationBlock

public JmlConfigurationBlock(org.eclipse.jdt.internal.ui.wizards.IStatusChangeListener context,
                             IProject project,
                             org.eclipse.ui.preferences.IWorkbenchPreferenceContainer container)

Method Detail

dispose

public void dispose()

Overrides:

dispose in class org.eclipse.jdt.internal.ui.preferences.OptionsConfigurationBlock