org.processmining.plugins.tsanalyzer.gui

Class GUIPropertyInteger

    • Field Summary

      Fields 
      Modifier and Type Field and Description
      protected boolean myEditable 
      protected int myWidth 
    • Constructor Summary

      Constructors 
      Constructor and Description
      GUIPropertyInteger(java.lang.String name, int defaultValue, int minValue, int maxValue)
      Creates an integer property without a discription and notification.
      GUIPropertyInteger(java.lang.String name, int defaultValue, int minValue, int maxValue, GuiNotificationTarget target)
      Creates an integer property without a discription.
      GUIPropertyInteger(java.lang.String name, java.lang.String description, int defaultValue, GuiNotificationTarget target, int width, boolean editable)
      Creates an integer property without a minimal and minimal value.
      GUIPropertyInteger(java.lang.String name, java.lang.String description, int defaultValue, int minValue, int maxValue)
      Creates an integer property without notification.
      GUIPropertyInteger(java.lang.String name, java.lang.String description, int defaultValue, int minValue, int maxValue, GuiNotificationTarget target, int width, boolean editable)
      Creates an integer property.
    • Method Summary

      Methods 
      Modifier and Type Method and Description
      void disable()
      Prevents that this property may be manipulated via the GUI panel.
      void enable()
      Re-activates the possibility to manipulate this property via the GUI panel.
      javax.swing.JPanel getPropertyPanel()
      Creates GUI panel containg this property, ready to display in some settings dialog.
      int getValue()
      The method to be invoked when the value of this property is to be used.
      boolean isEnabled()
      Checks whether the spinner is currently enabled or disabled.
      void setValue(int value)
      Sets the value of this property
      void stateChanged(javax.swing.event.ChangeEvent e)
      The method automatically invoked when changing the spinner status.
      • Methods inherited from class java.lang.Object

        clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
    • Field Detail

      • myWidth

        protected int myWidth
      • myEditable

        protected boolean myEditable
    • Constructor Detail

      • GUIPropertyInteger

        public GUIPropertyInteger(java.lang.String name,
                          int defaultValue,
                          int minValue,
                          int maxValue)
        Creates an integer property without a discription and notification.
        Parameters:
        name - the name of this property
        defaultValue - the default value of this property
        minValue - the minimal value that can be assigned to this property
        maxValue - the maximal value that can be assigned to this property
      • GUIPropertyInteger

        public GUIPropertyInteger(java.lang.String name,
                          java.lang.String description,
                          int defaultValue,
                          int minValue,
                          int maxValue)
        Creates an integer property without notification.
        Parameters:
        name - the name of this property
        description - of this property (to be displayed as a tool tip)
        defaultValue - the default value of this property
        minValue - the minimal value that can be assigned to this property
        maxValue - the maximal value that can be assigned to this property
      • GUIPropertyInteger

        public GUIPropertyInteger(java.lang.String name,
                          int defaultValue,
                          int minValue,
                          int maxValue,
                          GuiNotificationTarget target)
        Creates an integer property without a discription.
        Parameters:
        name - the name of this property
        defaultValue - the default value of this property
        minValue - the minimal value that can be assigned to this property
        maxValue - the maximal value that can be assigned to this property
        target - the object to be notified as soon the state of this property changes
      • GUIPropertyInteger

        public GUIPropertyInteger(java.lang.String name,
                          java.lang.String description,
                          int defaultValue,
                          int minValue,
                          int maxValue,
                          GuiNotificationTarget target,
                          int width,
                          boolean editable)
        Creates an integer property.
        Parameters:
        name - the name of this property
        description - of this property (to be displayed as a tool tip)
        defaultValue - the default value of this property
        minValue - the minimal value that can be assigned to this property
        maxValue - the maximal value that can be assigned to this property
        target - the object to be notified as soon the state of this property changes
      • GUIPropertyInteger

        public GUIPropertyInteger(java.lang.String name,
                          java.lang.String description,
                          int defaultValue,
                          GuiNotificationTarget target,
                          int width,
                          boolean editable)
        Creates an integer property without a minimal and minimal value.
        Parameters:
        name - the name of this property
        description - of this property (to be displayed as a tool tip)
        defaultValue - the default value of this property
        target - the object to be notified as soon the state of this property changes
    • Method Detail

      • stateChanged

        public void stateChanged(javax.swing.event.ChangeEvent e)
        The method automatically invoked when changing the spinner status.
        Specified by:
        stateChanged in interface javax.swing.event.ChangeListener
        Parameters:
        e - The passed change event (not used).
      • getValue

        public int getValue()
        The method to be invoked when the value of this property is to be used.
        Returns:
        the current value of this property
      • isEnabled

        public boolean isEnabled()
        Checks whether the spinner is currently enabled or disabled.
        Returns:
        true if is enabled, false otherwise
      • disable

        public void disable()
        Prevents that this property may be manipulated via the GUI panel.
        See Also:
        enable()
      • enable

        public void enable()
        Re-activates the possibility to manipulate this property via the GUI panel.
        See Also:
        disable()
      • setValue

        public void setValue(int value)
        Sets the value of this property
        Parameters:
        value - double
      • getPropertyPanel

        public javax.swing.JPanel getPropertyPanel()
        Creates GUI panel containg this property, ready to display in some settings dialog.
        Returns:
        the graphical panel representing this property