Raptor
Class ProofBox

java.lang.Object
  Raptor.ProofItem
      Raptor.ProofBox

All Implemented Interfaces:

java.awt.event.ActionListener, java.awt.event.MouseListener, java.io.Serializable, java.util.EventListener

public class ProofBox
extends ProofItem
implements java.awt.event.MouseListener, java.awt.event.ActionListener, java.io.Serializable

Implements a box in a proof.
Extends ProofItem, so a proof is made up of a list of ProofItems.
Contains a linked list of ProofItems, which make up the lines of the proof in the box.

See Also:

Serialized Form

Field Summary

int

skolem

Constructor Summary

ProofBox(ProofLine pGoal, ProofWindow pParentWindow, ProofBox pParentBox)
Constructs a ProofBox (with Goal).

ProofBox(ProofWindow pParentWindow)
Constructs a ProofBox (Outer).

ProofBox(ProofWindow pParentWindow, ProofBox pParentBox)
Constructs a ProofBox.

Method Summary

void	actionPerformed(java.awt.event.ActionEvent pEvent) Handles actions performed within the ProofWindow
void	addItem(int pIndex, ProofItem pItem) Adds ProofItem to specified position in LinkedList of ProofItems.
void	addItem(ProofItem pItem) Adds ProofItem to the LinkedList of ProofItems in the ProofBox.
void	addSkolems(ProofBox pParBox, PanSignature pTemp)
void	addToSignature(java.util.List<Atom> pNewAtoms) Adds the given list of Atoms to the signature of the ProofBox.
void	cleanup() Removes the empty line before a goal line when that goal has become proved but there are still goals remaining in the proof.
void	deselectAll() Used to deselect the items once a rule has been executed or the rule failed to execute.
javax.swing.JPanel	display() Returns the ProofBox within a JPanel.
boolean	getDisplayBorder() Returns true is the box is displayed.
boolean	getDisplayItems() Returns true if box's ProofItems are not hidden, otherwise false.
int	getIndex(ProofItem pCurrent) Returns the index of a given ProofItem
int	getInvCount() Returns the invCount (invariant count)
PanSignature	getMainSignature()
ProofBox	getNextBox() Returns the next ProofBox in the list.
ProofBox	getOlderSiblingBox() Returns the ProofBox that references this ProofBox as its nextBox.
ProofItem	getProofItem(int i) Returns the ith in the ProofItems list
java.util.List<ProofItem>	getProofItems() Returns the list of ProofItems contained in the box.
PanSignature	getSignature() Returns the signature of the ProofBox.
int	getUnknownCount() Returns the unknownCount
boolean	hasNextBox() A ProofBox item in a proof may be a list of ProofBoxes.
void	incrementInvCount() Increments the invCount
void	incrementUnknownCount() Increments the unknownCount
boolean	isProved() Returns true if the box has been proved
boolean	isVertical() Returns true if orientation of ProofBox is vertical.
void	mouseClicked(java.awt.event.MouseEvent e) Responds to a ProofBox with a mouse listener being clicked.
ProofItem	next(ProofItem pCurrent) Returns the next ProofItem in the ProofItems list
int[]	recalculateLineNum(int pFirstProofLine, int pFirstProgLine) Recalculates the line numbers within the ProofBox.
void	regenerate(ProofBox pOutsideBox, ProofWindow pParentWindow) Copies (this) ProofBox to the given outsideBox.
void	removeItem(int pIndex) Removes the specified item from the list of ProofItems
void	setBoxStarted(boolean pOption) Sets if the box has been started or not
void	setDashedBox(boolean pOption) Controls the appearance of the ProofBox.
void	setDisplayBorder(boolean pOption) Used to set the display options of the ProofBox.
void	setDisplayItems(boolean pOption) Controls if the content of the ProofBox should be displayed.
void	setInvCount(int pInvCount) Sets the invCount to value pInvCount
ProofBox	setNextBox() Creates a new ProofBox to follow the current ProofBox and returns this new sibling ProofBox.
void	setOlderSiblingBox(ProofBox pSibling) Sets the olderSiblingBox of this ProofBox as the ProofBox that refernces this ProofBox as its nextBox.
void	setUnknownCount(int pUnknownCount) Sets the unknownCount to value pUnknownCount
void	setVertical(boolean pOpt) Controls if sibling boxes should be displayed vertically.

Methods inherited from class Raptor.ProofItem

deselectLine, deselectLineNoClear, displayColour, getParentBox, getParentWindow, mouseEntered, mouseExited, mousePressed, mouseReleased, setParentBox

Methods inherited from class java.lang.Object

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

Methods inherited from interface java.awt.event.MouseListener

mouseEntered, mouseExited, mousePressed, mouseReleased

Field Detail

skolem

public int skolem

Constructor Detail

ProofBox

public ProofBox(ProofWindow pParentWindow)

Constructs a ProofBox (Outer).
Used to construct the outer ProofBox. Also used in conjunction with the Undo functionality and restores the necessary counts.

Parameters:

pParentWindow - The ProofWindow that the box is inside.

ProofBox

public ProofBox(ProofWindow pParentWindow,
                ProofBox pParentBox)

Constructs a ProofBox.
Used to construct a ProofBox inside a parent ProofBox.

Parameters:

pParentWindow - The ProofWindow that the box is inside.

pParentBox - The outer ProofBox that contains this ProofBox.

ProofBox

public ProofBox(ProofLine pGoal,
                ProofWindow pParentWindow,
                ProofBox pParentBox)

Constructs a ProofBox (with Goal).
Used to construct a ProofBox inside a parent ProofBox with an initialised goal.
Not currently used in Pandora implementation.

Parameters:

pGoal - The goal of the ProofBox

pParentWindow - The ProofWindow that the box is inside.

pParentBox - The outer ProofBox that contains this ProofBox.

Method Detail

getNextBox

public ProofBox getNextBox()

Returns the next ProofBox in the list.

setNextBox

public ProofBox setNextBox()

Creates a new ProofBox to follow the current ProofBox and returns this new sibling ProofBox.

hasNextBox

public boolean hasNextBox()

A ProofBox item in a proof may be a list of ProofBoxes.

getOlderSiblingBox

public ProofBox getOlderSiblingBox()

Returns the ProofBox that references this ProofBox as its nextBox.

setOlderSiblingBox

public void setOlderSiblingBox(ProofBox pSibling)

Sets the olderSiblingBox of this ProofBox as the ProofBox that refernces this ProofBox as its nextBox.

Parameters:

pSibling - older sibling of this ProofBox

setBoxStarted

public void setBoxStarted(boolean pOption)

Sets if the box has been started or not

Parameters:

pOption - set if proof has been started for the box yet

isProved

public boolean isProved()

Returns true if the box has been proved

getDisplayBorder

public boolean getDisplayBorder()

Returns true is the box is displayed.
Returns false when the box has been compressed.

setDisplayBorder

public void setDisplayBorder(boolean pOption)

Used to set the display options of the ProofBox.

Parameters:

pOption - Box is displayed when true, otherwise hidden

getDisplayItems

public boolean getDisplayItems()

Returns true if box's ProofItems are not hidden, otherwise false.

setDisplayItems

public void setDisplayItems(boolean pOption)

Controls if the content of the ProofBox should be displayed.

Parameters:

pOption - Box is displayed when true, otherwise hidden

setDashedBox

public void setDashedBox(boolean pOption)

Controls the appearance of the ProofBox.
i.e. whether the ProofBox has dashed or solid borders.

Parameters:

pOption - A dashed line ProofBox is displayed when true

isVertical

public boolean isVertical()

Returns true if orientation of ProofBox is vertical. For XMLEncoder

setVertical

public void setVertical(boolean pOpt)

Controls if sibling boxes should be displayed vertically.

Parameters:

pOpt - set true to display the boxes vertically

getUnknownCount

public int getUnknownCount()

Returns the unknownCount

setUnknownCount

public void setUnknownCount(int pUnknownCount)

Sets the unknownCount to value pUnknownCount

Parameters:

pUnknownCount - value to set unknownCount

incrementUnknownCount

public void incrementUnknownCount()

Increments the unknownCount

getInvCount

public int getInvCount()

Returns the invCount (invariant count)

setInvCount

public void setInvCount(int pInvCount)

Sets the invCount to value pInvCount

Parameters:

pInvCount - value to set invCount

incrementInvCount

public void incrementInvCount()

Increments the invCount

getProofItems

public java.util.List<ProofItem> getProofItems()

Returns the list of ProofItems contained in the box.

recalculateLineNum

public int[] recalculateLineNum(int pFirstProofLine,
                                int pFirstProgLine)

Recalculates the line numbers within the ProofBox.

Specified by:

recalculateLineNum in class ProofItem

Parameters:

pFirstProofLine - The value of the first ProofLine in the ProofBox

pFirstProgLine - the value o fhe first ProgramLine in the ProofBox

next

public ProofItem next(ProofItem pCurrent)

Returns the next ProofItem in the ProofItems list

Parameters:

pCurrent - current ProofItem

getIndex

public int getIndex(ProofItem pCurrent)

Returns the index of a given ProofItem

Parameters:

pCurrent - current ProofItem

getProofItem

public ProofItem getProofItem(int i)

Returns the ith in the ProofItems list

Parameters:

i - ProofItem to return

addItem

public void addItem(ProofItem pItem)

Adds ProofItem to the LinkedList of ProofItems in the ProofBox.
Appends the item to the end of List.

Parameters:

pItem - ProofItem to be added

addItem

public void addItem(int pIndex,
                    ProofItem pItem)

Adds ProofItem to specified position in LinkedList of ProofItems.

Parameters:

pIndex - Position to add

pItem - ProofItem to be added

removeItem

public void removeItem(int pIndex)

Removes the specified item from the list of ProofItems

Parameters:

pIndex - Index of ProofItem to be removed

addSkolems

public void addSkolems(ProofBox pParBox,
                       PanSignature pTemp)

addToSignature

public void addToSignature(java.util.List<Atom> pNewAtoms)

Adds the given list of Atoms to the signature of the ProofBox.
Only Atoms not already in the signature are added to the signture.

Parameters:

pNewAtoms - the atoms to be added to the signature

getSignature

public PanSignature getSignature()

Returns the signature of the ProofBox.

getMainSignature

public PanSignature getMainSignature()

deselectAll

public void deselectAll()

Used to deselect the items once a rule has been executed or the rule failed to execute.

display

public javax.swing.JPanel display()

Returns the ProofBox within a JPanel.

Specified by:

display in class ProofItem

mouseClicked

public void mouseClicked(java.awt.event.MouseEvent e)

Responds to a ProofBox with a mouse listener being clicked.

Specified by:

mouseClicked in interface java.awt.event.MouseListener

Overrides:

mouseClicked in class ProofItem

Parameters:

e - the object with a mouse listener that was clicked

cleanup

public void cleanup()

Removes the empty line before a goal line when that goal has become proved but there are still goals remaining in the proof.

regenerate

public void regenerate(ProofBox pOutsideBox,
                       ProofWindow pParentWindow)

Copies (this) ProofBox to the given outsideBox.
It is recreated to ensure ActionListeners function.

Parameters:

pOutsideBox - destination of regenerated ProofBox

pParentWindow - window which the current and new ProofBox belong to

actionPerformed

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

Handles actions performed within the ProofWindow

Specified by:

actionPerformed in interface java.awt.event.ActionListener