edu.mit.csail.sdg.alloy4graph
Class GraphViewer

java.lang.Object
  java.awt.Component
      java.awt.Container
          javax.swing.JComponent
              javax.swing.JPanel
                  edu.mit.csail.sdg.alloy4graph.GraphViewer

All Implemented Interfaces:

java.awt.image.ImageObserver, java.awt.MenuContainer, java.io.Serializable, javax.accessibility.Accessible

public final class GraphViewer
extends javax.swing.JPanel

This class displays the graph.

Thread Safety: Can be called only by the AWT event thread.

See Also:

Serialized Form

Nested Class Summary

Nested classes/interfaces inherited from class javax.swing.JPanel

javax.swing.JPanel.AccessibleJPanel

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

javax.swing.JPopupMenu

pop The right-click context menu associated with this JPanel.

Fields inherited from class javax.swing.JComponent

accessibleContext, 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

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

GraphViewer(Graph graph)
Construct a GraphViewer that displays the given graph.

Method Summary

java.lang.Object	alloyGetAnnotationAtXY(int mouseX, int mouseY) Returns the annotation for the node or edge at location x,y (or null if none)
java.lang.Object	alloyGetHighlightedAnnotation() Returns the annotation for the currently highlighted node/edge (or null if none)
java.lang.Object	alloyGetSelectedAnnotation() Returns the annotation for the currently selected node/edge (or null if none)
void	alloyPopup(java.awt.Component c, int x, int y) Show the popup menu at location (x,y)
void	alloyRepaint() Repaint this component.
void	alloySaveAs() Export the current drawing as a PNG or PDF file by asking the user for the filename and the image resolution.
void	alloySaveAsPDF(java.lang.String filename, int dpi) Export the current drawing as a PDF file with the given image resolution.
void	alloySaveAsPNG(java.lang.String filename, double scale, double dpiX, double dpiY) Export the current drawing as a PNG file with the given file name and image resolution.
java.awt.Dimension	getPreferredSize() Returns the preferred size of this component.
void	paintComponent(java.awt.Graphics gr) This method is called by Swing to draw this component.
java.lang.String	toString() Returns a DOT representation of the current graph.

Methods inherited from class javax.swing.JPanel

getAccessibleContext, getUI, getUIClassID, paramString, setUI, updateUI

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, getVerifyInputWhenFocusTarget, getVetoableChangeListeners, getVisibleRect, getWidth, getX, getY, grabFocus, isDoubleBuffered, isLightweightComponent, isManagingFocus, isOpaque, isOptimizedDrawingEnabled, isPaintingForPrint, isPaintingTile, isRequestFocusEnabled, isValidateRoot, paint, paintBorder, paintChildren, paintImmediately, paintImmediately, 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

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, transferFocusBackward, 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, 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, getPeer, getPropertyChangeListeners, getPropertyChangeListeners, getSize, getToolkit, getTreeLock, gotFocus, handleEvent, hasFocus, hide, 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, resize, resize, setBounds, setBounds, setComponentOrientation, setCursor, setDropTarget, setFocusable, setFocusTraversalKeysEnabled, setIgnoreRepaint, setLocale, setLocation, setLocation, setName, setSize, setSize, show, show, size, transferFocus, transferFocusUpCycle

Methods inherited from class java.lang.Object

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

Field Detail

pop

public final javax.swing.JPopupMenu pop

The right-click context menu associated with this JPanel.

Constructor Detail

GraphViewer

public GraphViewer(Graph graph)

Construct a GraphViewer that displays the given graph.

Method Detail

alloyGetAnnotationAtXY

public java.lang.Object alloyGetAnnotationAtXY(int mouseX,
                                               int mouseY)

Returns the annotation for the node or edge at location x,y (or null if none)

alloyGetSelectedAnnotation

public java.lang.Object alloyGetSelectedAnnotation()

Returns the annotation for the currently selected node/edge (or null if none)

alloyGetHighlightedAnnotation

public java.lang.Object alloyGetHighlightedAnnotation()

Returns the annotation for the currently highlighted node/edge (or null if none)

alloyRepaint

public void alloyRepaint()

Repaint this component.

alloySaveAs

public void alloySaveAs()

Export the current drawing as a PNG or PDF file by asking the user for the filename and the image resolution.

alloySaveAsPDF

public void alloySaveAsPDF(java.lang.String filename,
                           int dpi)
                    throws java.io.IOException

Export the current drawing as a PDF file with the given image resolution.

Throws:

java.io.IOException

alloySaveAsPNG

public void alloySaveAsPNG(java.lang.String filename,
                           double scale,
                           double dpiX,
                           double dpiY)
                    throws java.io.IOException

Export the current drawing as a PNG file with the given file name and image resolution.

Throws:

java.io.IOException

alloyPopup

public void alloyPopup(java.awt.Component c,
                       int x,
                       int y)

Show the popup menu at location (x,y)

toString

public java.lang.String toString()

Returns a DOT representation of the current graph.

Overrides:

toString in class java.awt.Component

getPreferredSize

public java.awt.Dimension getPreferredSize()

Returns the preferred size of this component.

Overrides:

getPreferredSize in class javax.swing.JComponent

paintComponent

public void paintComponent(java.awt.Graphics gr)

This method is called by Swing to draw this component.

Overrides:

paintComponent in class javax.swing.JComponent