Raptor
Class ProofWindow

java.lang.Object
  java.awt.Component
      java.awt.Container
          javax.swing.JComponent
              javax.swing.JPanel
                  Raptor.ProofWindow

All Implemented Interfaces:

java.awt.event.ActionListener, java.awt.event.FocusListener, java.awt.event.KeyListener, java.awt.image.ImageObserver, java.awt.MenuContainer, java.io.Serializable, java.util.EventListener, javax.accessibility.Accessible

public class ProofWindow
extends javax.swing.JPanel
implements java.awt.event.ActionListener, java.awt.event.KeyListener, java.awt.event.FocusListener

Everything contained within each tab is a ProofWindow. This includes mainProofBox and the buttons for applying rules.

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

ProofItem	firstTMLine
boolean	inProof
ProofBox	mainProofBox
java.util.List<ProofBox>	redoList
java.util.List<ProofLine>	tempProofLines
java.util.List<ProofLine>	TMProofLines
java.util.List<ProofBox>	undoList
View	view

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

ProofWindow(View pFrame)
Creates a new ProofWindow

ProofWindow(View pFrame, java.lang.String pDeclarations, java.lang.String pMethodPre, java.lang.String pMethodPost, java.lang.String pRetType, java.lang.String pRes)

Method Summary

void	actionPerformed(java.awt.event.ActionEvent pEvent) Handles actions performed within the ProofWindow
void	addConstant() Adds a Constant to the signature
void	addFunction() Adds a Function to the signature
void	addPredicate() Adds a Predicate to the signature
void	addToMainProofBox(ProofItem pItem) Adds a ProofItem to the mainProofBox
void	addToPost(java.lang.String pInput) Adds the input string to post
void	addToPre(java.lang.String pInput) Adds the input string to pre
void	addToProgram(java.lang.String pInput) Adds the input string to program
void	clearLastRuleSelected() Resets the button which was last selected
void	clearLastSelectedLine() Deselects the selected ProofItem
void	clearPostInput() Clears the postcondition input
void	clearPreInput() Clears the precondition input
void	clearProgramInput() Clears the program input
void	commitSaveState() Adds the temporarily stored copy of the ProofBox to the undo list and clears all the redo states.
void	deselectRule(javax.swing.JButton pRule) Clears the button to be deselected
void	disableButtons() Used when a TM rule is invoked which disables all rule buttons
void	displayAllSignature() Updates the contents of all signature display boxes
void	enableButtons() Used when a TM rule is completed which enables all rule buttons
void	finishedRule() Performed when a rule application has been completed.
void	focusGained(java.awt.event.FocusEvent e) Invoked when a component gains the keyboard focus
void	focusLost(java.awt.event.FocusEvent e) Invoked when a component loses the keyboard focus
javax.swing.JButton	getLastRuleSelected() Returns the button which was last selected
java.lang.String	getPost() Gets the postcondition input
java.lang.String	getPre() Gets the precondition input
java.lang.String	getProgram() Gets the program input
ProofBox	getProofBox()
PanSignature	getSignature() Returns the signature of ProofWindow
void	inputProofMode() Mode for inputting data into the proof.
boolean	isDone()
void	keyPressed(java.awt.event.KeyEvent e) Handle the key pressed event
void	keyReleased(java.awt.event.KeyEvent e) Handle the key released event
void	keyTyped(java.awt.event.KeyEvent e) Handle the key typed event
void	openProof(java.lang.String pFilename) Deserializes the given/goal or proofBox from given file location. Please see the comment for saveProof, it may be a better idea to store the files in an XML format.
void	redo() Redoes rules which have been undone
void	reloadProofBox() Refreshes the outermost mainProofBox in the ProofWindow
void	saveProof(java.lang.String pFilename) Serializes the given/goal or proofBox to given file location. I would prefer to encode this into XML.
void	selectRule(javax.swing.JButton pRule) Sets the button which was last selected.
void	setLastSelectedLine(ProofItem pLine) Changes the new selected ProofItem and deselects previous ones
void	setupMainProofBox() Resets the mainProofBox display for solveProofMode()
void	showGlobalSignature() Displays the global signature
void	showLocalSignature(PanSignature pLocalSig) Displays the local signature
void	showSignature() Shows the signature in sidebar
void	solveProofMode() Mode for solving proof by applying rules.
void	undo() Undoes rules which have been applied to the ProofBox.

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, getPreferredSize, 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, paintComponent, 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, toString, transferFocus, transferFocusUpCycle

Methods inherited from class java.lang.Object

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

Field Detail

view

public View view

inProof

public boolean inProof

tempProofLines

public java.util.List<ProofLine> tempProofLines

TMProofLines

public java.util.List<ProofLine> TMProofLines

undoList

public java.util.List<ProofBox> undoList

redoList

public java.util.List<ProofBox> redoList

mainProofBox

public ProofBox mainProofBox

firstTMLine

public ProofItem firstTMLine

Constructor Detail

ProofWindow

public ProofWindow(View pFrame)

Creates a new ProofWindow

Parameters:

pFrame - the View associated with the ProofWindow

ProofWindow

public ProofWindow(View pFrame,
                   java.lang.String pDeclarations,
                   java.lang.String pMethodPre,
                   java.lang.String pMethodPost,
                   java.lang.String pRetType,
                   java.lang.String pRes)

Method Detail

inputProofMode

public void inputProofMode()

Mode for inputting data into the proof.

solveProofMode

public void solveProofMode()

Mode for solving proof by applying rules.

getSignature

public PanSignature getSignature()

Returns the signature of ProofWindow

actionPerformed

public void actionPerformed(java.awt.event.ActionEvent pEvent)

Handles actions performed within the ProofWindow

Specified by:

actionPerformed in interface java.awt.event.ActionListener

keyTyped

public void keyTyped(java.awt.event.KeyEvent e)

Handle the key typed event

Specified by:

keyTyped in interface java.awt.event.KeyListener

keyPressed

public void keyPressed(java.awt.event.KeyEvent e)

Handle the key pressed event

Specified by:

keyPressed in interface java.awt.event.KeyListener

keyReleased

public void keyReleased(java.awt.event.KeyEvent e)

Handle the key released event

Specified by:

keyReleased in interface java.awt.event.KeyListener

focusGained

public void focusGained(java.awt.event.FocusEvent e)

Invoked when a component gains the keyboard focus

Specified by:

focusGained in interface java.awt.event.FocusListener

focusLost

public void focusLost(java.awt.event.FocusEvent e)

Invoked when a component loses the keyboard focus

Specified by:

focusLost in interface java.awt.event.FocusListener

openProof

public void openProof(java.lang.String pFilename)

Deserializes the given/goal or proofBox from given file location.

Please see the comment for saveProof, it may be a better idea to store the files in an XML format.

Parameters:

pFilename - destination of saved file

saveProof

public void saveProof(java.lang.String pFilename)

Serializes the given/goal or proofBox to given file location.

I would prefer to encode this into XML. The Java API mentions that using serialization for long term storage is not a good idea since it won't be compatible with future versions of Swing. To store ProofBox as XML, it would require a custom persistence delegate to instantiate the class because ProofBox lacks a no-argument constructor.

XMLEncoder xml = new XMLEncoder(
new BufferedOutputStream(
new FileOutputStream(filename)));

Parameters:

pFilename - destination of saved file

undo

public void undo()

Undoes rules which have been applied to the ProofBox.

redo

public void redo()

Redoes rules which have been undone

commitSaveState

public void commitSaveState()

Adds the temporarily stored copy of the ProofBox to the undo list and clears all the redo states. saveState() and commitSaveState() are separated so only successful applications of rules are saved

reloadProofBox

public void reloadProofBox()

Refreshes the outermost mainProofBox in the ProofWindow

setupMainProofBox

public void setupMainProofBox()

Resets the mainProofBox display for solveProofMode()

setLastSelectedLine

public void setLastSelectedLine(ProofItem pLine)

Changes the new selected ProofItem and deselects previous ones

Parameters:

pLine - the selected ProofLine or ProgramLine

clearLastSelectedLine

public void clearLastSelectedLine()

Deselects the selected ProofItem

getLastRuleSelected

public javax.swing.JButton getLastRuleSelected()

Returns the button which was last selected

clearLastRuleSelected

public void clearLastRuleSelected()

Resets the button which was last selected

selectRule

public void selectRule(javax.swing.JButton pRule)

Sets the button which was last selected. Alters the button's colour

Parameters:

pRule - last selected button

deselectRule

public void deselectRule(javax.swing.JButton pRule)

Clears the button to be deselected

Parameters:

pRule - button which has been deselected

finishedRule

public void finishedRule()

Performed when a rule application has been completed. Rule is exited, buttons and lines are cleared, etc.

displayAllSignature

public void displayAllSignature()

Updates the contents of all signature display boxes

addPredicate

public void addPredicate()

Adds a Predicate to the signature

addConstant

public void addConstant()

Adds a Constant to the signature

addFunction

public void addFunction()

Adds a Function to the signature

clearPreInput

public void clearPreInput()

Clears the precondition input

getPre

public java.lang.String getPre()

Gets the precondition input

addToPre

public void addToPre(java.lang.String pInput)

Adds the input string to pre

Parameters:

pInput - the precondition input String

clearProgramInput

public void clearProgramInput()

Clears the program input

getProgram

public java.lang.String getProgram()

Gets the program input

addToProgram

public void addToProgram(java.lang.String pInput)

Adds the input string to program

Parameters:

pInput - the program input String

clearPostInput

public void clearPostInput()

Clears the postcondition input

getPost

public java.lang.String getPost()

Gets the postcondition input

addToPost

public void addToPost(java.lang.String pInput)

Adds the input string to post

Parameters:

pInput - the post input String

addToMainProofBox

public void addToMainProofBox(ProofItem pItem)

Adds a ProofItem to the mainProofBox

Parameters:

pItem - new ProofItem to be added

showSignature

public void showSignature()

Shows the signature in sidebar

showGlobalSignature

public void showGlobalSignature()

Displays the global signature

showLocalSignature

public void showLocalSignature(PanSignature pLocalSig)

Displays the local signature

Parameters:

pLocalSig - local signature to display

disableButtons

public void disableButtons()

Used when a TM rule is invoked which disables all rule buttons

enableButtons

public void enableButtons()

Used when a TM rule is completed which enables all rule buttons

isDone

public boolean isDone()

getProofBox

public ProofBox getProofBox()