org.jmlspecs.checker
Class JmlGUI

java.lang.Object
  java.awt.Component
      java.awt.Container
          java.awt.Window
              java.awt.Frame
                  javax.swing.JFrame
                      org.multijava.util.gui.GUIFrame
                          org.multijava.util.gui.GUI
                              org.jmlspecs.checker.JmlGUI

All Implemented Interfaces:

Accessible, ImageObserver, MenuContainer, RootPaneContainer, Serializable, TransferHandler.HasGetTransferHandler, WindowConstants

public class JmlGUI

extends org.multijava.util.gui.GUI

This class is automatically generated from JmlGUI.gui and contains member fields corresponding to tool-specific GUI specifications.

Nested Class Summary
protected  class	JmlGUI.AllFilesGUIFileFilter
protected  class	JmlGUI.JmlCompilation
protected  class	JmlGUI.JmlGUIFileFilter
protected  class	JmlGUI.JmlOpenHandler

 

Nested classes inherited from class org.multijava.util.gui.GUI

org.multijava.util.gui.GUI.Compilation, org.multijava.util.gui.GUI.GUIFileFilter, org.multijava.util.gui.GUI.OpenHandler

 

Nested classes inherited from class javax.swing.JFrame

JFrame.AccessibleJFrame

 

Nested classes inherited from class java.awt.Frame

Frame.AccessibleAWTFrame

 

Nested classes inherited from class java.awt.Window

Window.AccessibleAWTWindow

 

Nested classes inherited from class java.awt.Container

Container.AccessibleAWTContainer

 

Nested classes inherited from class java.awt.Component

Component.AccessibleAWTComponent, Component.BaselineResizeBehavior, Component.BltBufferStrategy, Component.FlipBufferStrategy

 

Field Summary

 

Fields inherited from class org.multijava.util.gui.GUI

 

Fields inherited from class org.multijava.util.gui.GUIFrame

currentDirectory, preferences, toolName

 

Fields inherited from class javax.swing.JFrame

accessibleContext, EXIT_ON_CLOSE, rootPane, rootPaneCheckingEnabled

 

Fields inherited from class java.awt.Frame

CROSSHAIR_CURSOR, DEFAULT_CURSOR, E_RESIZE_CURSOR, HAND_CURSOR, ICONIFIED, MAXIMIZED_BOTH, MAXIMIZED_HORIZ, MAXIMIZED_VERT, MOVE_CURSOR, N_RESIZE_CURSOR, NE_RESIZE_CURSOR, NORMAL, NW_RESIZE_CURSOR, S_RESIZE_CURSOR, SE_RESIZE_CURSOR, SW_RESIZE_CURSOR, TEXT_CURSOR, W_RESIZE_CURSOR, WAIT_CURSOR

 

Fields inherited from class java.awt.Window

 

Fields inherited from class java.awt.Container

 

Fields inherited from class java.awt.Component

BOTTOM_ALIGNMENT, CENTER_ALIGNMENT, LEFT_ALIGNMENT, RIGHT_ALIGNMENT, TOP_ALIGNMENT

 

Fields inherited from interface javax.swing.WindowConstants

DISPOSE_ON_CLOSE, DO_NOTHING_ON_CLOSE, HIDE_ON_CLOSE

 

Fields inherited from interface java.awt.image.ImageObserver

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

 

Constructor Summary

JmlGUI(Options options, ArrayList infiles, boolean commandLine, boolean standAlone)

 

Method Summary
protected  org.multijava.util.gui.GUI.Compilation	createCompilationInstance(String[] files, Options opt, OutputStream os)
protected  org.multijava.util.gui.GUI.OpenHandler	createOpenHandlerInstance()
protected  org.multijava.util.gui.GUIOutputWindow	createOutputWindow(InputStream is)
protected  boolean	dirInClassPath(Options opt, String dir)
protected  String	getClasspath(Options opt)
protected  String	getSourcepath(Options opt)
protected  String	getWebpageLocation()
protected  String	getWebpageName()
static JmlGUI	init(String[] args, boolean standAlone)
void	interruptCompilation()
static void	main(String[] args)

 

Methods inherited from class org.multijava.util.gui.GUI

clearPreferences, closeWindowOperations, getGUIWindowPreferences, getMinimumSize, getPreferredSize, preferencesHaveChanged, savePreferences, setClearPrefsEnabled, setCurrentLookAndFeelEnabled, setLookAndFeel, setLookAndFeel, setSavePrefsEnabled

 

Methods inherited from class org.multijava.util.gui.GUIFrame

getMaximumSize, lookAndFeelHasChanged, putCurrentDirectory, putLookAndFeel, setCurrentDirectory

 

Methods inherited from class javax.swing.JFrame

addImpl, createRootPane, frameInit, getAccessibleContext, getContentPane, getDefaultCloseOperation, getGlassPane, getGraphics, getJMenuBar, getLayeredPane, getRootPane, getTransferHandler, isDefaultLookAndFeelDecorated, isRootPaneCheckingEnabled, paramString, processWindowEvent, remove, repaint, setContentPane, setDefaultCloseOperation, setDefaultLookAndFeelDecorated, setGlassPane, setIconImage, setJMenuBar, setLayeredPane, setLayout, setRootPane, setRootPaneCheckingEnabled, setTransferHandler, update

 

Methods inherited from class java.awt.Frame

addNotify, getCursorType, getExtendedState, getFrames, getIconImage, getMaximizedBounds, getMenuBar, getState, getTitle, isResizable, isUndecorated, remove, removeNotify, setCursor, setExtendedState, setMaximizedBounds, setMenuBar, setResizable, setState, setTitle, setUndecorated

 

Methods inherited from class java.awt.Window

addPropertyChangeListener, addPropertyChangeListener, addWindowFocusListener, addWindowListener, addWindowStateListener, applyResourceBundle, applyResourceBundle, createBufferStrategy, createBufferStrategy, dispose, getBufferStrategy, getFocusableWindowState, getFocusCycleRootAncestor, getFocusOwner, getFocusTraversalKeys, getGraphicsConfiguration, getIconImages, getInputContext, getListeners, getLocale, getModalExclusionType, getMostRecentFocusOwner, getOwnedWindows, getOwner, getOwnerlessWindows, getToolkit, getWarningString, getWindowFocusListeners, getWindowListeners, getWindows, getWindowStateListeners, hide, isActive, isAlwaysOnTop, isAlwaysOnTopSupported, isFocusableWindow, isFocusCycleRoot, isFocused, isLocationByPlatform, isShowing, pack, postEvent, processEvent, processWindowFocusEvent, processWindowStateEvent, removeWindowFocusListener, removeWindowListener, removeWindowStateListener, reshape, setAlwaysOnTop, setBounds, setBounds, setCursor, setFocusableWindowState, setFocusCycleRoot, setIconImages, setLocationByPlatform, setLocationRelativeTo, setMinimumSize, setModalExclusionType, setSize, setSize, setVisible, show, toBack, toFront

 

Methods inherited from class java.awt.Container

add, add, add, add, add, addContainerListener, applyComponentOrientation, areFocusTraversalKeysSet, countComponents, deliverEvent, doLayout, findComponentAt, findComponentAt, getAlignmentX, getAlignmentY, getComponent, getComponentAt, getComponentAt, getComponentCount, getComponents, getComponentZOrder, getContainerListeners, getFocusTraversalPolicy, getInsets, getLayout, getMousePosition, insets, invalidate, isAncestorOf, isFocusCycleRoot, isFocusTraversalPolicyProvider, isFocusTraversalPolicySet, layout, list, list, locate, minimumSize, paint, paintComponents, preferredSize, print, printComponents, processContainerEvent, remove, removeAll, removeContainerListener, setComponentZOrder, setFocusTraversalKeys, setFocusTraversalPolicy, setFocusTraversalPolicyProvider, setFont, 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, contains, createImage, createImage, createVolatileImage, createVolatileImage, disable, disableEvents, dispatchEvent, enable, enable, enableEvents, enableInputMethods, firePropertyChange, firePropertyChange, firePropertyChange, firePropertyChange, firePropertyChange, firePropertyChange, firePropertyChange, firePropertyChange, firePropertyChange, getBackground, getBaseline, getBaselineResizeBehavior, getBounds, getBounds, getColorModel, getComponentListeners, getComponentOrientation, getCursor, getDropTarget, getFocusListeners, getFocusTraversalKeysEnabled, getFont, getFontMetrics, getForeground, getHeight, getHierarchyBoundsListeners, getHierarchyListeners, getIgnoreRepaint, getInputMethodListeners, getInputMethodRequests, getKeyListeners, getLocation, getLocation, getLocationOnScreen, getMouseListeners, getMouseMotionListeners, getMousePosition, getMouseWheelListeners, getName, getParent, getPeer, getPropertyChangeListeners, getPropertyChangeListeners, getSize, getSize, getTreeLock, getWidth, getX, getY, gotFocus, handleEvent, hasFocus, imageUpdate, inside, isBackgroundSet, isCursorSet, isDisplayable, isDoubleBuffered, isEnabled, isFocusable, isFocusOwner, isFocusTraversable, isFontSet, isForegroundSet, isLightweight, isMaximumSizeSet, isMinimumSizeSet, isOpaque, isPreferredSizeSet, isValid, isVisible, keyDown, keyUp, list, list, list, location, lostFocus, mouseDown, mouseDrag, mouseEnter, mouseExit, mouseMove, mouseUp, move, nextFocus, paintAll, prepareImage, prepareImage, printAll, processComponentEvent, processFocusEvent, processHierarchyBoundsEvent, processHierarchyEvent, processInputMethodEvent, processKeyEvent, processMouseEvent, processMouseMotionEvent, processMouseWheelEvent, removeComponentListener, removeFocusListener, removeHierarchyBoundsListener, removeHierarchyListener, removeInputMethodListener, removeKeyListener, removeMouseListener, removeMouseMotionListener, removeMouseWheelListener, removePropertyChangeListener, removePropertyChangeListener, repaint, repaint, repaint, requestFocus, requestFocus, requestFocusInWindow, requestFocusInWindow, resize, resize, setBackground, setComponentOrientation, setDropTarget, setEnabled, setFocusable, setFocusTraversalKeysEnabled, setForeground, setIgnoreRepaint, setLocale, setLocation, setLocation, setMaximumSize, setName, setPreferredSize, show, size, toString, transferFocus, transferFocusUpCycle

 

Methods inherited from class java.lang.Object

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

 

Methods inherited from interface java.awt.MenuContainer

getFont, postEvent

 

Constructor Detail

JmlGUI

public JmlGUI(Options options,
              ArrayList infiles,
              boolean commandLine,
              boolean standAlone)

main

public static void main(String[] args)

init

public static JmlGUI init(String[] args,
                          boolean standAlone)

interruptCompilation

public void interruptCompilation()

dirInClassPath

protected boolean dirInClassPath(Options opt,
                                 String dir)

getClasspath

protected String getClasspath(Options opt)

getSourcepath

protected String getSourcepath(Options opt)

createOpenHandlerInstance

protected org.multijava.util.gui.GUI.OpenHandler createOpenHandlerInstance()

createCompilationInstance

protected org.multijava.util.gui.GUI.Compilation createCompilationInstance(String[] files,
                                                                           Options opt,
                                                                           OutputStream os)

getWebpageName

protected String getWebpageName()

getWebpageLocation

protected String getWebpageLocation()

createOutputWindow

protected org.multijava.util.gui.GUIOutputWindow createOutputWindow(InputStream is)