public class InfoTreeNode
extends javax.swing.tree.DefaultMutableTreeNode
InfoTree
is an instance of this class.Constructor and Description |
---|
InfoTreeNode(BuiltInRule br,
java.util.Properties ruleExplanations) |
Modifier and Type | Method and Description |
---|---|
Rule |
getRule() |
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, toString
public InfoTreeNode(BuiltInRule br, java.util.Properties ruleExplanations)
public Rule getRule()
Copyright © 2003-2019 The KeY-Project.