Package org.processmining.objectcentricconstraintchecking.algorithms.editor

Class EditorRuler

  • All Implemented Interfaces:
    java.awt.dnd.DropTargetListener, java.awt.event.MouseMotionListener, java.awt.image.ImageObserver, java.awt.MenuContainer, java.io.Serializable, java.util.EventListener
    public class EditorRuler
extends javax.swing.JComponent
implements java.awt.event.MouseMotionListener, java.awt.dnd.DropTargetListener
    Component that displays a ruler for a JGraph component.
    See Also:
    Serialized Form

    • Nested Class Summary

      • Nested classes/interfaces inherited from class javax.swing.JComponent

        javax.swing.JComponent.AccessibleJComponent

      • Nested classes/interfaces inherited from class java.awt.Container

        java.awt.Container.AccessibleAWTContainer

      • Nested classes/interfaces inherited from class java.awt.Component

        java.awt.Component.AccessibleAWTComponent, java.awt.Component.BaselineResizeBehavior, java.awt.Component.BltBufferStrategy, java.awt.Component.FlipBufferStrategy

    • Field Summary

      Fields 
      Modifier and Type Field Description
      protected int activelength
      Specified that start and length of the active region, ie the region to paint with the background border.
      protected int activeoffset
      Specified that start and length of the active region, ie the region to paint with the background border.
      protected static boolean DEFAULT_ISMETRIC
      Internal constant used to describe the screen resolution (DPI).
      protected static int DEFAULT_PAGESCALE
      Internal constant used to describe the screen resolution (DPI).
      protected mxGraphComponent graphComponent
      Reference to the attached graph.
      protected java.awt.Color inactiveBackground
      Defines the inactive background border.
      protected static int INCH
      Internal constant used to describe the screen resolution (DPI).
      protected double increment
      Parameters to control the display.
      protected java.awt.Font labelFont  
      protected boolean metric
      Specifies the unit system.
      protected java.awt.Point mouse
      Holds the current and first mouse point.
      static java.text.NumberFormat numberFormat
      Holds the shared number formatter.
      protected int orientation
      Specifies the orientation.
      static int ORIENTATION_HORIZONTAL
      Defines the constants for horizontal and vertical orientation.
      static int ORIENTATION_VERTICAL
      Defines the constants for horizontal and vertical orientation.
      protected mxEventSource.mxIEventListener repaintHandler  
      protected int rulerSize
      Specifies height or width of the ruler.
      protected double scale
      Specifies the scale for the metrics.
      protected int tickDistance
      Specifies the minimum distance between two major ticks.
      protected double units
      Parameters to control the display.

      • Fields inherited from class javax.swing.JComponent

        listenerList, TOOL_TIP_TEXT_KEY, ui, UNDEFINED_CONDITION, WHEN_ANCESTOR_OF_FOCUSED_COMPONENT, WHEN_FOCUSED, WHEN_IN_FOCUSED_WINDOW

      • Fields inherited from class java.awt.Component

        accessibleContext, BOTTOM_ALIGNMENT, CENTER_ALIGNMENT, LEFT_ALIGNMENT, RIGHT_ALIGNMENT, TOP_ALIGNMENT

      • Fields inherited from interface java.awt.image.ImageObserver

        ABORT, ALLBITS, ERROR, FRAMEBITS, HEIGHT, PROPERTIES, SOMEBITS, WIDTH

    • Constructor Summary

      Constructors 
      Constructor Description
      EditorRuler​(mxGraphComponent graphComponent, int orientation)
      Constructs a new ruler for the specified graph and orientation.

    • Method Summary

      All Methods Instance Methods Concrete Methods 
      Modifier and Type Method Description
      void dragEnter​(java.awt.dnd.DropTargetDragEvent arg0)  
      void dragExit​(java.awt.dnd.DropTargetEvent arg0)  
      void dragOver​(java.awt.dnd.DropTargetDragEvent arg0)  
      void drop​(java.awt.dnd.DropTargetDropEvent arg0)  
      void dropActionChanged​(java.awt.dnd.DropTargetDragEvent arg0)  
      java.awt.Dimension getPreferredSize()
      Returns the preferred size by replacing the respective component of the graph's preferred size with rulerSize.
      int getRulerSize()
      Returns the ruler's horizontal or vertical size.
      int getTickDistance()  
      boolean isMetric()
      Returns true if the ruler uses metric units.
      void mouseDragged​(java.awt.event.MouseEvent e)  
      void mouseMoved​(java.awt.event.MouseEvent e)  
      void paintComponent​(java.awt.Graphics g)
      Paints the ruler.
      void repaint​(int x, int y)
      Repaints the ruler between the specified 0 and x or y depending on the orientation.
      void setActiveLength​(int length)
      Sets the length of the active region in pixels.
      void setActiveOffset​(int offset)
      Sets the start of the active region in pixels.
      void setMetric​(boolean isMetric)
      Sets if the ruler uses metric units.
      void setRulerSize​(int rulerSize)
      Sets the ruler's horizontal or vertical size.
      void setTickDistance​(int tickDistance)  
      protected void updateIncrementAndUnits()
      Updates the local variables used for painting based on the current scale and unit system.
      protected void updateMousePosition​(java.awt.Point pt)
      Repaints the mouse position.

      • Methods inherited from class javax.swing.JComponent

        addAncestorListener, addNotify, addVetoableChangeListener, computeVisibleRect, contains, createToolTip, disable, enable, firePropertyChange, firePropertyChange, firePropertyChange, fireVetoableChange, getActionForKeyStroke, getActionMap, getAlignmentX, getAlignmentY, getAncestorListeners, getAutoscrolls, getBaseline, getBaselineResizeBehavior, getBorder, getBounds, getClientProperty, getComponentGraphics, getComponentPopupMenu, getConditionForKeyStroke, getDebugGraphicsOptions, getDefaultLocale, getFontMetrics, getGraphics, getHeight, getInheritsPopupMenu, getInputMap, getInputMap, getInputVerifier, getInsets, getInsets, getListeners, getLocation, getMaximumSize, getMinimumSize, getNextFocusableComponent, getPopupLocation, getRegisteredKeyStrokes, getRootPane, getSize, getToolTipLocation, getToolTipText, getToolTipText, getTopLevelAncestor, getTransferHandler, getUI, getUIClassID, getVerifyInputWhenFocusTarget, getVetoableChangeListeners, getVisibleRect, getWidth, getX, getY, grabFocus, hide, isDoubleBuffered, isLightweightComponent, isManagingFocus, isOpaque, isOptimizedDrawingEnabled, isPaintingForPrint, isPaintingOrigin, isPaintingTile, isRequestFocusEnabled, isValidateRoot, paint, paintBorder, paintChildren, paintImmediately, paintImmediately, paramString, print, printAll, printBorder, printChildren, printComponent, processComponentKeyEvent, processKeyBinding, processKeyEvent, processMouseEvent, processMouseMotionEvent, putClientProperty, registerKeyboardAction, registerKeyboardAction, removeAncestorListener, removeNotify, removeVetoableChangeListener, repaint, repaint, requestDefaultFocus, requestFocus, requestFocus, requestFocusInWindow, requestFocusInWindow, resetKeyboardActions, reshape, revalidate, scrollRectToVisible, setActionMap, setAlignmentX, setAlignmentY, setAutoscrolls, setBackground, setBorder, setComponentPopupMenu, setDebugGraphicsOptions, setDefaultLocale, setDoubleBuffered, setEnabled, setFocusTraversalKeys, setFont, setForeground, setInheritsPopupMenu, setInputMap, setInputVerifier, setMaximumSize, setMinimumSize, setNextFocusableComponent, setOpaque, setPreferredSize, setRequestFocusEnabled, setToolTipText, setTransferHandler, setUI, setVerifyInputWhenFocusTarget, setVisible, unregisterKeyboardAction, update, updateUI

      • Methods inherited from class java.awt.Container

        add, add, add, add, add, addContainerListener, addImpl, addPropertyChangeListener, addPropertyChangeListener, applyComponentOrientation, areFocusTraversalKeysSet, countComponents, deliverEvent, doLayout, findComponentAt, findComponentAt, getComponent, getComponentAt, getComponentAt, getComponentCount, getComponents, getComponentZOrder, getContainerListeners, getFocusTraversalKeys, getFocusTraversalPolicy, getLayout, getMousePosition, insets, invalidate, isAncestorOf, isFocusCycleRoot, isFocusCycleRoot, isFocusTraversalPolicyProvider, isFocusTraversalPolicySet, layout, list, list, locate, minimumSize, paintComponents, preferredSize, printComponents, processContainerEvent, processEvent, remove, remove, removeAll, removeContainerListener, setComponentZOrder, setFocusCycleRoot, setFocusTraversalPolicy, setFocusTraversalPolicyProvider, setLayout, transferFocusDownCycle, validate, validateTree

      • Methods inherited from class java.awt.Component

        action, add, addComponentListener, addFocusListener, addHierarchyBoundsListener, addHierarchyListener, addInputMethodListener, addKeyListener, addMouseListener, addMouseMotionListener, addMouseWheelListener, bounds, checkImage, checkImage, coalesceEvents, contains, createImage, createImage, createVolatileImage, createVolatileImage, disableEvents, dispatchEvent, enable, enableEvents, enableInputMethods, firePropertyChange, firePropertyChange, firePropertyChange, firePropertyChange, firePropertyChange, firePropertyChange, getAccessibleContext, getBackground, getBounds, getColorModel, getComponentListeners, getComponentOrientation, getCursor, getDropTarget, getFocusCycleRootAncestor, getFocusListeners, getFocusTraversalKeysEnabled, getFont, getForeground, getGraphicsConfiguration, getHierarchyBoundsListeners, getHierarchyListeners, getIgnoreRepaint, getInputContext, getInputMethodListeners, getInputMethodRequests, getKeyListeners, getLocale, getLocation, getLocationOnScreen, getMouseListeners, getMouseMotionListeners, getMousePosition, getMouseWheelListeners, getName, getParent, getPropertyChangeListeners, getPropertyChangeListeners, getSize, getToolkit, getTreeLock, gotFocus, handleEvent, hasFocus, imageUpdate, inside, isBackgroundSet, isCursorSet, isDisplayable, isEnabled, isFocusable, isFocusOwner, isFocusTraversable, isFontSet, isForegroundSet, isLightweight, isMaximumSizeSet, isMinimumSizeSet, isPreferredSizeSet, isShowing, isValid, isVisible, keyDown, keyUp, list, list, list, location, lostFocus, mouseDown, mouseDrag, mouseEnter, mouseExit, mouseMove, mouseUp, move, nextFocus, paintAll, postEvent, prepareImage, prepareImage, processComponentEvent, processFocusEvent, processHierarchyBoundsEvent, processHierarchyEvent, processInputMethodEvent, processMouseWheelEvent, remove, removeComponentListener, removeFocusListener, removeHierarchyBoundsListener, removeHierarchyListener, removeInputMethodListener, removeKeyListener, removeMouseListener, removeMouseMotionListener, removeMouseWheelListener, removePropertyChangeListener, removePropertyChangeListener, repaint, repaint, repaint, requestFocus, requestFocus, requestFocusInWindow, resize, resize, setBounds, setBounds, setComponentOrientation, setCursor, setDropTarget, setFocusable, setFocusTraversalKeysEnabled, setIgnoreRepaint, setLocale, setLocation, setLocation, setMixingCutoutShape, setName, setSize, setSize, show, show, size, toString, transferFocus, transferFocusBackward, transferFocusUpCycle

      • Methods inherited from class java.lang.Object

        clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

    • Field Detail

      • ORIENTATION_HORIZONTAL

        public static int ORIENTATION_HORIZONTAL
        Defines the constants for horizontal and vertical orientation.

      • ORIENTATION_VERTICAL

        public static int ORIENTATION_VERTICAL
        Defines the constants for horizontal and vertical orientation.

      • INCH

        protected static int INCH
        Internal constant used to describe the screen resolution (DPI). Default is 72.

      • DEFAULT_PAGESCALE

        protected static int DEFAULT_PAGESCALE
        Internal constant used to describe the screen resolution (DPI). Default is 72.

      • DEFAULT_ISMETRIC

        protected static boolean DEFAULT_ISMETRIC
        Internal constant used to describe the screen resolution (DPI). Default is 72.

      • numberFormat

        public static final java.text.NumberFormat numberFormat
        Holds the shared number formatter.
        See Also:
        NumberFormat.getInstance()

      • inactiveBackground

        protected java.awt.Color inactiveBackground
        Defines the inactive background border. Default is a not-so-dark gray.

      • orientation

        protected int orientation
        Specifies the orientation.

      • activeoffset

        protected int activeoffset
        Specified that start and length of the active region, ie the region to paint with the background border. This is used for example to indicate the printable region of a graph.

      • activelength

        protected int activelength
        Specified that start and length of the active region, ie the region to paint with the background border. This is used for example to indicate the printable region of a graph.

      • scale

        protected double scale
        Specifies the scale for the metrics. Default is JGraphEditorDiagramPane#DEFAULT_PAGESCALE.

      • metric

        protected boolean metric
        Specifies the unit system. Default is JGraphEditorDiagramPane#DEFAULT_ISMETRIC.

      • labelFont

        protected java.awt.Font labelFont

      • rulerSize

        protected int rulerSize
        Specifies height or width of the ruler. Default is 15 pixels.

      • tickDistance

        protected int tickDistance
        Specifies the minimum distance between two major ticks. Default is 30.

      • graphComponent

        protected mxGraphComponent graphComponent
        Reference to the attached graph.

      • mouse

        protected java.awt.Point mouse
        Holds the current and first mouse point.

      • increment

        protected double increment
        Parameters to control the display.

      • units

        protected double units
        Parameters to control the display.

    • Constructor Detail

      • EditorRuler

        public EditorRuler​(mxGraphComponent graphComponent,
                   int orientation)
        Constructs a new ruler for the specified graph and orientation.
        Parameters:
        graph - The graph to create the ruler for.
        orientation - The orientation to use for the ruler.

    • Method Detail

      • setActiveOffset

        public void setActiveOffset​(int offset)
        Sets the start of the active region in pixels.
        Parameters:
        offset - The start of the active region.

      • setActiveLength

        public void setActiveLength​(int length)
        Sets the length of the active region in pixels.
        Parameters:
        length - The length of the active region.

      • isMetric

        public boolean isMetric()
        Returns true if the ruler uses metric units.
        Returns:
        Returns if the ruler is metric.

      • setMetric

        public void setMetric​(boolean isMetric)
        Sets if the ruler uses metric units.
        Parameters:
        isMetric - Whether to use metric units.

      • getRulerSize

        public int getRulerSize()
        Returns the ruler's horizontal or vertical size.
        Returns:
        Returns the rulerSize.

      • setRulerSize

        public void setRulerSize​(int rulerSize)
        Sets the ruler's horizontal or vertical size.
        Parameters:
        rulerSize - The rulerSize to set.

      • setTickDistance

        public void setTickDistance​(int tickDistance)

      • getTickDistance

        public int getTickDistance()

      • getPreferredSize

        public java.awt.Dimension getPreferredSize()
        Returns the preferred size by replacing the respective component of the graph's preferred size with rulerSize.
        Overrides:
        getPreferredSize in class javax.swing.JComponent
        Returns:
        Returns the preferred size for the ruler.

      • dragEnter

        public void dragEnter​(java.awt.dnd.DropTargetDragEvent arg0)
        Specified by:
        dragEnter in interface java.awt.dnd.DropTargetListener

      • dragExit

        public void dragExit​(java.awt.dnd.DropTargetEvent arg0)
        Specified by:
        dragExit in interface java.awt.dnd.DropTargetListener

      • dragOver

        public void dragOver​(java.awt.dnd.DropTargetDragEvent arg0)
        Specified by:
        dragOver in interface java.awt.dnd.DropTargetListener

      • drop

        public void drop​(java.awt.dnd.DropTargetDropEvent arg0)
        Specified by:
        drop in interface java.awt.dnd.DropTargetListener

      • dropActionChanged

        public void dropActionChanged​(java.awt.dnd.DropTargetDragEvent arg0)
        Specified by:
        dropActionChanged in interface java.awt.dnd.DropTargetListener

      • mouseMoved

        public void mouseMoved​(java.awt.event.MouseEvent e)
        Specified by:
        mouseMoved in interface java.awt.event.MouseMotionListener

      • mouseDragged

        public void mouseDragged​(java.awt.event.MouseEvent e)
        Specified by:
        mouseDragged in interface java.awt.event.MouseMotionListener

      • updateMousePosition

        protected void updateMousePosition​(java.awt.Point pt)
        Repaints the mouse position.

      • updateIncrementAndUnits

        protected void updateIncrementAndUnits()
        Updates the local variables used for painting based on the current scale and unit system.

      • repaint

        public void repaint​(int x,
                    int y)
        Repaints the ruler between the specified 0 and x or y depending on the orientation.
        Parameters:
        x - The endpoint for repainting a horizontal ruler.
        y - The endpoint for repainting a vertical ruler.

      • paintComponent

        public void paintComponent​(java.awt.Graphics g)
        Paints the ruler.
        Overrides:
        paintComponent in class javax.swing.JComponent
        Parameters:
        g - The graphics to paint the ruler to.