de.uka.ilkd.key.proof.mgt

Class BasicTask

java.lang.Object

javax.swing.tree.DefaultMutableTreeNode

de.uka.ilkd.key.proof.mgt.BasicTask

All Implemented Interfaces:

TaskTreeNode, java.io.Serializable, java.lang.Cloneable, javax.swing.tree.MutableTreeNode, javax.swing.tree.TreeNode

public class BasicTask
extends javax.swing.tree.DefaultMutableTreeNode
implements TaskTreeNode

Captures a node in the TaskTree which contains exactly one proof. Such a node is the only one with a one to one mapping between TaskTreeNode and Proof. It may be a sub task of a more complex task such as ProofListTask.

See Also:

Serialized Form

Field Summary

Fields

Modifier and Type	Field and Description
private ProofAggregate	proof
private static long	serialVersionUID

Fields inherited from class javax.swing.tree.DefaultMutableTreeNode

allowsChildren, children, EMPTY_ENUMERATION, parent, userObject

Fields inherited from interface de.uka.ilkd.key.proof.mgt.TaskTreeNode

NO_CHILDREN

Constructor Summary

Constructors

Constructor and Description
BasicTask(ProofAggregate pl) creates a task with a single proof.

Method Summary

Modifier and Type	Method and Description
Proof[]	allProofs() returns all proofs attached to this basic task
void	decoupleFromEnv() removes the associated proof from their environment
TaskTreeNode[]	getChildren()
ProofEnvironment	getProofEnv()
TaskTreeNode	getRootTask() returns the upper most task this basic task belongs to.
ProofStatus	getStatus() asks the proof management component of the associated proofs for the status of the associated proof .
void	insertNode(TaskTreeModel model, javax.swing.tree.MutableTreeNode parentNode) inserts a node given the task tree model and a parent node
Proof	proof()
java.lang.String	shortDescr()
java.lang.String	toString()

Methods inherited from class javax.swing.tree.DefaultMutableTreeNode

add, breadthFirstEnumeration, children, clone, depthFirstEnumeration, getAllowsChildren, getChildAfter, getChildAt, getChildBefore, getChildCount, getDepth, getFirstChild, getFirstLeaf, getIndex, getLastChild, getLastLeaf, getLeafCount, getLevel, getNextLeaf, getNextNode, getNextSibling, getParent, getPath, getPathToRoot, getPreviousLeaf, getPreviousNode, getPreviousSibling, getRoot, getSharedAncestor, getSiblingCount, getUserObject, getUserObjectPath, insert, isLeaf, isNodeAncestor, isNodeChild, isNodeDescendant, isNodeRelated, isNodeSibling, isRoot, pathFromAncestorEnumeration, postorderEnumeration, preorderEnumeration, remove, remove, removeAllChildren, removeFromParent, setAllowsChildren, setParent, setUserObject

Methods inherited from class java.lang.Object

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

Methods inherited from interface de.uka.ilkd.key.proof.mgt.TaskTreeNode

getPath

Methods inherited from interface javax.swing.tree.MutableTreeNode

insert, remove, remove, removeFromParent, setParent, setUserObject

Methods inherited from interface javax.swing.tree.TreeNode

children, getAllowsChildren, getChildAt, getChildCount, getIndex, getParent, isLeaf

Field Detail

serialVersionUID

private static final long serialVersionUID

See Also:

Constant Field Values

proof

private ProofAggregate proof

Constructor Detail

BasicTask

public BasicTask(ProofAggregate pl)

creates a task with a single proof. The given proof list must contain exactly one proof.

Method Detail

shortDescr

public java.lang.String shortDescr()

Specified by:

shortDescr in interface TaskTreeNode

toString

public java.lang.String toString()

Overrides:

toString in class javax.swing.tree.DefaultMutableTreeNode

getProofEnv

public ProofEnvironment getProofEnv()

Specified by:

getProofEnv in interface TaskTreeNode

proof

public Proof proof()

Specified by:

proof in interface TaskTreeNode

allProofs

public Proof[] allProofs()

returns all proofs attached to this basic task

Specified by:

allProofs in interface TaskTreeNode

insertNode

public void insertNode(TaskTreeModel model,
                       javax.swing.tree.MutableTreeNode parentNode)

inserts a node given the task tree model and a parent node

Specified by:

insertNode in interface TaskTreeNode

getStatus

public ProofStatus getStatus()

asks the proof management component of the associated proofs for the status of the associated proof .

Specified by:

getStatus in interface TaskTreeNode

getRootTask

public TaskTreeNode getRootTask()

returns the upper most task this basic task belongs to.

decoupleFromEnv

public void decoupleFromEnv()

removes the associated proof from their environment

Specified by:

decoupleFromEnv in interface TaskTreeNode

getChildren

public TaskTreeNode[] getChildren()

Specified by:

getChildren in interface TaskTreeNode