Pandora
Class ProofWindow

java.lang.Object
  java.awt.Component
      java.awt.Container
          javax.swing.JComponent
              javax.swing.JPanel
                  Pandora.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
RuleController	ruleCtrl
static long	serialVersionUID
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 frame)
Creates a new ProofWindow.

Method Summary

void	actionPerformed(java.awt.event.ActionEvent event) Performs actions performed within the ProofWindow
void	addConstant() Adds a Constant to the signature
void	addFunction() Adds a Function to the signature
void	addLineToProof(Formula input, java.lang.String type) Adds a ProofLine while in solveProofMode
void	addPredicate() Adds a Predicate to the signature
void	addToGiven(java.lang.String input) Allows a string to be appended to the givens text box in enterProofMode
void	addToGoal(java.lang.String input) Allows a string to be appended to the goal text box in enterProofMode
void	clearLastRuleSelected() Resets the button which was last selected
void	clearLastSelectedLine() Deselects the selected ProofItem
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 rule) Clears the button to be deselected
void	disableButtons() Used when a TM rule is invoked which disables all rule buttons
void	displayAllSignature() Updatse 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
ProofBox	getProofBox()
PanSignature	getSignature()
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 filename) 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 main proof box in the ProofWindow
void	removeAllGiven() Removes all the input for givens in the enterProofMode
void	removeAllGoal() Removes all the input for goal in the enterProofMode
void	saveProof(java.lang.String filename) 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(ProofLine line) Changes the new selected ProofItem and deselects previous ones
void	setupMainProofBox()
void	showGlobalSignature() Displays the global signature
void	showLocalSignature(PanSignature localSig)
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

serialVersionUID

public static final long serialVersionUID

See Also:

Constant Field Values

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

ruleCtrl

public RuleController ruleCtrl

mainProofBox

public ProofBox mainProofBox

firstTMLine

public ProofItem firstTMLine

Constructor Detail

ProofWindow

public ProofWindow(View frame)

Creates a new ProofWindow.

Parameters:

frame - Store the View associated with the ProofWindow

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()

actionPerformed

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

Performs 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 filename)

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:

filename - destination of saved file

saveProof

public void saveProof(java.lang.String filename)

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:

filename - 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 seperated so only successful applications of rules are saved

reloadProofBox

public void reloadProofBox()

Refreshes the outermost main proof box in the ProofWindow

setupMainProofBox

public void setupMainProofBox()

setLastSelectedLine

public void setLastSelectedLine(ProofLine line)

Changes the new selected ProofItem and deselects previous ones

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:

rule - last selected button

deselectRule

public void deselectRule(javax.swing.JButton rule)

Clears the button to be deselected

Parameters:

rule - 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()

Updatse 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

removeAllGiven

public void removeAllGiven()

Removes all the input for givens in the enterProofMode

removeAllGoal

public void removeAllGoal()

Removes all the input for goal in the enterProofMode

addToGiven

public void addToGiven(java.lang.String input)

Allows a string to be appended to the givens text box in enterProofMode

addToGoal

public void addToGoal(java.lang.String input)

Allows a string to be appended to the goal text box in enterProofMode

addLineToProof

public void addLineToProof(Formula input,
                           java.lang.String type)

Adds a ProofLine while in solveProofMode

Parameters:

input - Formula to be added

type - Justification for the line

showSignature

public void showSignature()

Shows the signature in sidebar

showGlobalSignature

public void showGlobalSignature()

Displays the global signature

showLocalSignature

public void showLocalSignature(PanSignature localSig)

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()