public class InfoTreeModel
extends javax.swing.tree.DefaultTreeModel
DefaultTreeModel
used by InfoTree
.Modifier and Type | Class and Description |
---|---|
private class |
InfoTreeModel.FunctionsNode |
private class |
InfoTreeModel.RulesNode |
private class |
InfoTreeModel.TermLabelsNode |
Modifier and Type | Field and Description |
---|---|
private static java.lang.String |
LEMMAS |
private static long |
serialVersionUID |
private static java.lang.String |
TACLET_BASE |
Constructor and Description |
---|
InfoTreeModel(Goal goal,
XMLResources xmlResources,
MainWindow mainWindow) |
Modifier and Type | Method and Description |
---|---|
private void |
insertAsLast(InfoTreeNode ins,
InfoTreeNode parent) |
addTreeModelListener, asksAllowsChildren, fireTreeNodesChanged, fireTreeNodesInserted, fireTreeNodesRemoved, fireTreeStructureChanged, getChild, getChildCount, getIndexOfChild, getListeners, getPathToRoot, getPathToRoot, getRoot, getTreeModelListeners, insertNodeInto, isLeaf, nodeChanged, nodesChanged, nodeStructureChanged, nodesWereInserted, nodesWereRemoved, reload, reload, removeNodeFromParent, removeTreeModelListener, setAsksAllowsChildren, setRoot, valueForPathChanged
private static final long serialVersionUID
private static final java.lang.String LEMMAS
private static final java.lang.String TACLET_BASE
public InfoTreeModel(Goal goal, XMLResources xmlResources, MainWindow mainWindow)
private void insertAsLast(InfoTreeNode ins, InfoTreeNode parent)