Class InternalFrame

java.lang.Object
  extended byjava.awt.Component
      extended byjava.awt.Container
          extended byjavax.swing.JComponent
              extended byjavax.swing.JInternalFrame
                  extended byInternalFrame
All Implemented Interfaces:
javax.accessibility.Accessible, java.awt.image.ImageObserver, java.awt.MenuContainer, javax.swing.RootPaneContainer, java.io.Serializable, javax.swing.WindowConstants

class InternalFrame
extends javax.swing.JInternalFrame

Ein InternalFrame kann von verschiedenen Typen sein, beispielsweise ein Editor-Fenster oder ein Ausgabefenster für Text/Html.


Nested Class Summary
 
Nested classes inherited from class javax.swing.JInternalFrame
javax.swing.JInternalFrame.AccessibleJInternalFrame, javax.swing.JInternalFrame.JDesktopIcon
 
Nested classes inherited from class javax.swing.JComponent
javax.swing.JComponent.AccessibleJComponent
 
Nested classes inherited from class java.awt.Container
java.awt.Container.AccessibleAWTContainer
 
Nested classes inherited from class java.awt.Component
java.awt.Component.AccessibleAWTComponent, java.awt.Component.BltBufferStrategy, java.awt.Component.FlipBufferStrategy
 
Field Summary
static int BYHAND
          Konstante zum Erzeugen eines Fensters zur manuellen Verifizierung (ohne Next-Button).
(package private)  javax.swing.JPanel cp
          Liefert das aktuell bearbeitete Panel.
static int EDITOR
          Konstante zum Erzeugen eines Editor-Fensters.
static int HTMLOUT
          Konstante zum Erzeugen eines Html-Ausgabefensters.
static int NBYHAND
          Konstante zum Erzeugen eines Fensters zur manuellen Verifizierung (mit Next-Button).
static int TEXTOUT
          Konstante zum Erzeugen eines Text-Ausgabefensters.
static int VERIFOUT
          Konstante zum Erzeugen eines Fensters für die Ausgaben des Verifiers.
 
Fields inherited from class javax.swing.JInternalFrame
closable, CONTENT_PANE_PROPERTY, desktopIcon, FRAME_ICON_PROPERTY, frameIcon, GLASS_PANE_PROPERTY, iconable, IS_CLOSED_PROPERTY, IS_ICON_PROPERTY, IS_MAXIMUM_PROPERTY, IS_SELECTED_PROPERTY, isClosed, isIcon, isMaximum, isSelected, LAYERED_PANE_PROPERTY, maximizable, MENU_BAR_PROPERTY, resizable, ROOT_PANE_PROPERTY, rootPane, rootPaneCheckingEnabled, title, TITLE_PROPERTY
 
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.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, EXIT_ON_CLOSE, HIDE_ON_CLOSE
 
Fields inherited from interface java.awt.image.ImageObserver
ABORT, ALLBITS, ERROR, FRAMEBITS, HEIGHT, PROPERTIES, SOMEBITS, WIDTH
 
Constructor Summary
InternalFrame(int type, int posX, int posY, int width, int height, java.lang.String title, boolean resizable, boolean closable, boolean maximizable, boolean iconifiable)
          Erzeugt einen InternalFrame.
 
Method Summary
 void addText(java.lang.String text)
          Fügt Text in das Textfeld eines InternalFrames des Typs "EDITOR" oder "TEXTOUT" ein.
 void appendToLogFileString(java.lang.String appendix)
          Hängt an das Ende des logFileString die Zeichenkette appendix an.
 void copy()
          Zum Kopieren von Text aus dem Editorfeld.
 void cut()
          Zum Ausschneiden von Text aus dem Editorfeld.
 java.lang.String displayHtmlFile(java.lang.String file)
          Stellt eine Html-Datei in einem InternalFrame des Typs "HTMLOUT" dar.
 void focus()
          Setzt den Fokus auf ein Textfeld mit Syntax-Highlighting.
 javax.swing.JButton getAcceptButton()
          Liefert den Accept-Button
 int getConditionCounter()
          Liefert den Zähler der Verifikationsbedingungen.
 java.lang.String getFilename()
          Liefert den Namen der Ausgabedatei.
 javax.swing.JTextArea getJTextArea()
          Liefert das Ausgabe-Textfeld.
 java.lang.String getLogFileString()
          Liefert den Inhalt des logFileString.
 javax.swing.JButton getManualButton()
          Liefert den Manual-Button
 javax.swing.JButton getNewButton()
          Liefert den New-Button.
 javax.swing.JButton getNextButton()
          Liefert den Next-Button.
 SimpleNode getNode()
          Liefert den aktuellen Knoten, der dem Fenster zugrunde liegt.
 SimpleNode getOldNode()
          Liefert den Knoten, der durch Reset wiederhergestellt wird.
 javax.swing.JPanel getPanel()
          Liefert das Panel.
 java.lang.String getParseTree()
          Liefert den Parse-Tree des in der Eingabedatei spezifizierten Programms.
 SimpleNode getPtree()
          Liefert den aktuellen Teilbaum, der markiert wurde.
 javax.swing.JButton getResetButton()
          Liefert den Reset-Button
 java.lang.String getText()
          Liefert den Text eines InternalFrames des Typs "EDITOR".
 int getType()
          Liefert den Typ des InternalFrames.
 SimpleNode getUnModTree()
          Liefert den unveränderten vom Anwender ausgewählten Teilbaum
 VerifCondCreater getVerifCondCreater()
          Liefert den VerifCondCreater.
 void incConditionCounter()
          Erhöht den Zähler der Verifikationsbedingungen um 1.
 void paste()
          Zum Einfügen von Text in das Editorfeld.
 void recalculateVisibleLines()
          Berechnet die sichtbaren Zeilen des Textfeldes mit Syntax-Highlighting.
 void resetConditionCounter()
          Setzt den Zähler der Verifikationsbedingungen auf 1 zurück.
 void resetLogFileString()
          Setzt den logFileString zurück.
 void selectAll()
          Zum Markieren des kompletten Textes des Editorfeldes.
 void setCursor(int line, int column)
          Setzt den Cursor in einem Textfeld mit Syntax-Highlighting in Zeile line und Spalte column.
 void setFilename(java.lang.String filename)
          Setzt den Namen der Ausgabedatei.
 void setNode(SimpleNode tree)
          Definiert den aktuellen Knoten, der dem Fenster zugrunde liegt.
 void setOldNode(SimpleNode tree)
          Definiert den Knoten, der durch Reset wiederhergestellt wird.
 void setParseTree(java.lang.String parseTree)
          Setzt den Parse-Tree des in der Eingabedatei spezifizierten Programms.
 void setPtree(SimpleNode tree)
          Definiert den aktuellen Teilbaum, der markiert wurde.
 void setUnModTree(SimpleNode tree)
          Definiert den unveränderten vom Anwender ausgewählten Teilbaum
 void setVerifCondCreater(VerifCondCreater vcc)
          Setzt den VerifCondCreater.
 
Methods inherited from class javax.swing.JInternalFrame
addImpl, addInternalFrameListener, createRootPane, dispose, doDefaultCloseAction, fireInternalFrameEvent, getAccessibleContext, getContentPane, getDefaultCloseOperation, getDesktopIcon, getDesktopPane, getFocusCycleRootAncestor, getFocusOwner, getFrameIcon, getGlassPane, getInternalFrameListeners, getJMenuBar, getLayer, getLayeredPane, getMenuBar, getMostRecentFocusOwner, getNormalBounds, getRootPane, getTitle, getUI, getUIClassID, getWarningString, hide, isClosable, isClosed, isFocusCycleRoot, isIcon, isIconifiable, isMaximizable, isMaximum, isResizable, isRootPaneCheckingEnabled, isSelected, moveToBack, moveToFront, pack, paintComponent, paramString, remove, removeInternalFrameListener, reshape, restoreSubcomponentFocus, setClosable, setClosed, setContentPane, setDefaultCloseOperation, setDesktopIcon, setFocusCycleRoot, setFrameIcon, setGlassPane, setIcon, setIconifiable, setJMenuBar, setLayer, setLayer, setLayeredPane, setLayout, setMaximizable, setMaximum, setMenuBar, setNormalBounds, setResizable, setRootPane, setRootPaneCheckingEnabled, setSelected, setTitle, setUI, show, toBack, toFront, updateUI
 
Methods inherited from class javax.swing.JComponent
addAncestorListener, addNotify, addPropertyChangeListener, addPropertyChangeListener, addVetoableChangeListener, computeVisibleRect, contains, createToolTip, disable, enable, firePropertyChange, firePropertyChange, firePropertyChange, firePropertyChange, firePropertyChange, firePropertyChange, firePropertyChange, firePropertyChange, firePropertyChange, fireVetoableChange, getActionForKeyStroke, getActionMap, getAlignmentX, getAlignmentY, getAncestorListeners, getAutoscrolls, getBorder, getBounds, getClientProperty, getComponentGraphics, getConditionForKeyStroke, getDebugGraphicsOptions, getDefaultLocale, getGraphics, getHeight, getInputMap, getInputMap, getInputVerifier, getInsets, getInsets, getListeners, getLocation, getMaximumSize, getMinimumSize, getNextFocusableComponent, getPreferredSize, getPropertyChangeListeners, getPropertyChangeListeners, getRegisteredKeyStrokes, getSize, getToolTipLocation, getToolTipText, getToolTipText, getTopLevelAncestor, getTransferHandler, getVerifyInputWhenFocusTarget, getVetoableChangeListeners, getVisibleRect, getWidth, getX, getY, grabFocus, isDoubleBuffered, isLightweightComponent, isManagingFocus, isMaximumSizeSet, isMinimumSizeSet, isOpaque, isOptimizedDrawingEnabled, isPaintingTile, isPreferredSizeSet, isRequestFocusEnabled, isValidateRoot, paint, paintBorder, paintChildren, paintImmediately, paintImmediately, print, printAll, printBorder, printChildren, printComponent, processComponentKeyEvent, processKeyBinding, processKeyEvent, processMouseMotionEvent, putClientProperty, registerKeyboardAction, registerKeyboardAction, removeAncestorListener, removeNotify, removePropertyChangeListener, removePropertyChangeListener, removeVetoableChangeListener, repaint, repaint, requestDefaultFocus, requestFocus, requestFocus, requestFocusInWindow, requestFocusInWindow, resetKeyboardActions, revalidate, scrollRectToVisible, setActionMap, setAlignmentX, setAlignmentY, setAutoscrolls, setBackground, setBorder, setDebugGraphicsOptions, setDefaultLocale, setDoubleBuffered, setEnabled, setFont, setForeground, 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, applyComponentOrientation, areFocusTraversalKeysSet, countComponents, deliverEvent, doLayout, findComponentAt, findComponentAt, getComponent, getComponentAt, getComponentAt, getComponentCount, getComponents, getContainerListeners, getFocusTraversalKeys, getFocusTraversalPolicy, getLayout, insets, invalidate, isAncestorOf, isFocusCycleRoot, isFocusTraversalPolicySet, layout, list, list, locate, minimumSize, paintComponents, preferredSize, printComponents, processContainerEvent, processEvent, remove, removeAll, removeContainerListener, setFocusTraversalKeys, setFocusTraversalPolicy, 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, getBackground, getBounds, getColorModel, getComponentListeners, getComponentOrientation, getCursor, getDropTarget, getFocusListeners, getFocusTraversalKeysEnabled, getFont, getFontMetrics, getForeground, getGraphicsConfiguration, getHierarchyBoundsListeners, getHierarchyListeners, getIgnoreRepaint, getInputContext, getInputMethodListeners, getInputMethodRequests, getKeyListeners, getLocale, getLocation, getLocationOnScreen, getMouseListeners, getMouseMotionListeners, getMouseWheelListeners, getName, getParent, getPeer, getSize, getToolkit, getTreeLock, gotFocus, handleEvent, hasFocus, imageUpdate, inside, isBackgroundSet, isCursorSet, isDisplayable, isEnabled, isFocusable, isFocusOwner, isFocusTraversable, isFontSet, isForegroundSet, isLightweight, 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, processMouseEvent, processMouseWheelEvent, remove, removeComponentListener, removeFocusListener, removeHierarchyBoundsListener, removeHierarchyListener, removeInputMethodListener, removeKeyListener, removeMouseListener, removeMouseMotionListener, removeMouseWheelListener, repaint, repaint, repaint, resize, resize, setBounds, setBounds, setComponentOrientation, setCursor, setDropTarget, setFocusable, setFocusTraversalKeysEnabled, setIgnoreRepaint, setLocale, setLocation, setLocation, setName, setSize, setSize, show, size, toString, transferFocus, transferFocusUpCycle
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
 

Field Detail

EDITOR

public static final int EDITOR
Konstante zum Erzeugen eines Editor-Fensters.

See Also:
Constant Field Values

HTMLOUT

public static final int HTMLOUT
Konstante zum Erzeugen eines Html-Ausgabefensters.

See Also:
Constant Field Values

TEXTOUT

public static final int TEXTOUT
Konstante zum Erzeugen eines Text-Ausgabefensters.

See Also:
Constant Field Values

VERIFOUT

public static final int VERIFOUT
Konstante zum Erzeugen eines Fensters für die Ausgaben des Verifiers.

See Also:
Constant Field Values

cp

javax.swing.JPanel cp
Liefert das aktuell bearbeitete Panel.


BYHAND

public static final int BYHAND
Konstante zum Erzeugen eines Fensters zur manuellen Verifizierung (ohne Next-Button).

See Also:
Constant Field Values

NBYHAND

public static final int NBYHAND
Konstante zum Erzeugen eines Fensters zur manuellen Verifizierung (mit Next-Button).

See Also:
Constant Field Values
Constructor Detail

InternalFrame

public InternalFrame(int type,
                     int posX,
                     int posY,
                     int width,
                     int height,
                     java.lang.String title,
                     boolean resizable,
                     boolean closable,
                     boolean maximizable,
                     boolean iconifiable)
Erzeugt einen InternalFrame.

Parameters:
type - Typ des zu erzeugenden Fensters.
posX - x-Position der oberen linken Ecke des Fensters.
posY - y-Position der oberen linken Ecke des Fensters.
width - Breite des Fensters.
height - Höhe des Fensters.
title - Titel des Fensters.
resizable - Gibt an, ob die Grösse veränderbar sein soll.
closable - Gibt an, ob das "x" zum Schliessen in der Titelleiste sichtbar sein soll.
maximizable - Gibt an, ob das Symbol zum Maximieren in der Titelleiste sichtbar sein soll.
iconifiable - Gibt an, ob das Symbol zum Minimieren in der Titelleiste sichtbar sein soll.
Method Detail

getType

public int getType()
Liefert den Typ des InternalFrames.


getText

public java.lang.String getText()
Liefert den Text eines InternalFrames des Typs "EDITOR".


cut

public void cut()
Zum Ausschneiden von Text aus dem Editorfeld.


copy

public void copy()
Zum Kopieren von Text aus dem Editorfeld.


paste

public void paste()
Zum Einfügen von Text in das Editorfeld.


selectAll

public void selectAll()
Zum Markieren des kompletten Textes des Editorfeldes.


getJTextArea

public javax.swing.JTextArea getJTextArea()
Liefert das Ausgabe-Textfeld.


displayHtmlFile

public java.lang.String displayHtmlFile(java.lang.String file)
Stellt eine Html-Datei in einem InternalFrame des Typs "HTMLOUT" dar.

Parameters:
file - Name der Html-Datei.

addText

public void addText(java.lang.String text)
Fügt Text in das Textfeld eines InternalFrames des Typs "EDITOR" oder "TEXTOUT" ein.

Parameters:
text - Einzufügender Text.

recalculateVisibleLines

public void recalculateVisibleLines()
Berechnet die sichtbaren Zeilen des Textfeldes mit Syntax-Highlighting.
Ruft eine Methode des Syntax-Highlighting Packages auf.


setCursor

public void setCursor(int line,
                      int column)
Setzt den Cursor in einem Textfeld mit Syntax-Highlighting in Zeile line und Spalte column.


focus

public void focus()
Setzt den Fokus auf ein Textfeld mit Syntax-Highlighting.


getNextButton

public javax.swing.JButton getNextButton()
Liefert den Next-Button.


getManualButton

public javax.swing.JButton getManualButton()
Liefert den Manual-Button


getNewButton

public javax.swing.JButton getNewButton()
Liefert den New-Button.


getResetButton

public javax.swing.JButton getResetButton()
Liefert den Reset-Button


getAcceptButton

public javax.swing.JButton getAcceptButton()
Liefert den Accept-Button


setFilename

public void setFilename(java.lang.String filename)
Setzt den Namen der Ausgabedatei.


setParseTree

public void setParseTree(java.lang.String parseTree)
Setzt den Parse-Tree des in der Eingabedatei spezifizierten Programms.


getFilename

public java.lang.String getFilename()
Liefert den Namen der Ausgabedatei.


getParseTree

public java.lang.String getParseTree()
Liefert den Parse-Tree des in der Eingabedatei spezifizierten Programms.


appendToLogFileString

public void appendToLogFileString(java.lang.String appendix)
Hängt an das Ende des logFileString die Zeichenkette appendix an.


resetLogFileString

public void resetLogFileString()
Setzt den logFileString zurück.


getLogFileString

public java.lang.String getLogFileString()
Liefert den Inhalt des logFileString.


setVerifCondCreater

public void setVerifCondCreater(VerifCondCreater vcc)
Setzt den VerifCondCreater.


getVerifCondCreater

public VerifCondCreater getVerifCondCreater()
Liefert den VerifCondCreater.


incConditionCounter

public void incConditionCounter()
Erhöht den Zähler der Verifikationsbedingungen um 1.


getConditionCounter

public int getConditionCounter()
Liefert den Zähler der Verifikationsbedingungen.


resetConditionCounter

public void resetConditionCounter()
Setzt den Zähler der Verifikationsbedingungen auf 1 zurück.


getNode

public SimpleNode getNode()
Liefert den aktuellen Knoten, der dem Fenster zugrunde liegt.


getOldNode

public SimpleNode getOldNode()
Liefert den Knoten, der durch Reset wiederhergestellt wird.


getPtree

public SimpleNode getPtree()
Liefert den aktuellen Teilbaum, der markiert wurde.


getUnModTree

public SimpleNode getUnModTree()
Liefert den unveränderten vom Anwender ausgewählten Teilbaum


setNode

public void setNode(SimpleNode tree)
Definiert den aktuellen Knoten, der dem Fenster zugrunde liegt.

Parameters:
tree - SimpleNode, die in diesem Fenster bearbeitet wird

setOldNode

public void setOldNode(SimpleNode tree)
Definiert den Knoten, der durch Reset wiederhergestellt wird.

Parameters:
tree - SimpleNode, die der ursprünglich zu beweisenden Formel entspricht

setPtree

public void setPtree(SimpleNode tree)
Definiert den aktuellen Teilbaum, der markiert wurde.


setUnModTree

public void setUnModTree(SimpleNode tree)
Definiert den unveränderten vom Anwender ausgewählten Teilbaum


getPanel

public javax.swing.JPanel getPanel()
Liefert das Panel.