Class SpecExtensionEditor

  • All Implemented Interfaces:
    OptionsEditor, java.beans.PropertyChangeListener, java.util.EventListener

    public class SpecExtensionEditor
    extends java.lang.Object
    implements OptionsEditor, java.beans.PropertyChangeListener
    • Constructor Detail

      • SpecExtensionEditor

        public SpecExtensionEditor​(ProgramDB program)
    • Method Detail

      • reload

        public void reload()
        Description copied from interface: OptionsEditor
        A signal to reload the GUI widgets in the component created by this editor. This will happen when the options change out from under the editor, such as when the user restores the default options values.
        Specified by:
        reload in interface OptionsEditor
      • getEditorComponent

        public javax.swing.JComponent getEditorComponent​(Options options,
                                                         EditorStateFactory editorStateFactory)
        Description copied from interface: OptionsEditor
        Get the editor component.
        Specified by:
        getEditorComponent in interface OptionsEditor
        Parameters:
        options - The editable options that for which a GUI component will be created
        editorStateFactory - The factory that will provide state objects this options editor
      • propertyChange

        public void propertyChange​(java.beans.PropertyChangeEvent evt)
        Specified by:
        propertyChange in interface java.beans.PropertyChangeListener