public class InfoTreeModel
extends javax.swing.tree.DefaultTreeModel
DefaultTreeModel
used by InfoTree
.Constructor and Description |
---|
InfoTreeModel(Goal goal,
XMLResources xmlResources,
MainWindow mainWindow) |
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
public InfoTreeModel(Goal goal, XMLResources xmlResources, MainWindow mainWindow)
Copyright © 2003-2019 The KeY-Project.