    001    /* Copyright 2000, 2001, Compaq Computer Corporation */
    002
    003    package javafe.filespace;
    004
    005
    006    /**
    007     * A ExtTree is a HashTree that starts out as just a root node, but may
    008     * be extended at any time by (recursively) adding children.<p>
    009     *
    010     * Edges and nodes cannot be deleted once added, however.<p>
    011     */
    012
    013    class ExtTree extends HashTree {
    014
    015        /*
    016         * Object invariant: All elements in the edges HashTable are
    017         * ExtTrees.
    018         */
    019
    020
    021        /***************************************************
    022         *                                                 *
    023         * Creation:                                       *
    024         *                                                 *
    025         **************************************************/
    026
    027        /** Create a root node: */
    028        public ExtTree(Object data) {
    029            super(data);
    030        }
    031
    032        /** Create a non-root node: */
    033        //@ requires parent != null && label != null;
    034        protected ExtTree(Tree parent, String label, Object data) {
    035            super(parent, label, data);
    036        }
    037
    038
    039        /***************************************************
    040         *                                                 *
    041         * Adding children:                                *
    042         *                                                 *
    043         **************************************************/
    044
    045        /**
    046         * Create a new direct child of us with label label and data newData.
    047         * The new child will have no direct children.<p>
    048         *
    049         * If a child by the name of label already exists, then this
    050         * routine leaves the tree unchanged.<p>
    051         *
    052         * In either case, the (resulting) child with label label is returned.<p>
    053         */
    054        //@ requires label != null;
    055        //@ ensures \result != null;
    056        public ExtTree addChild(String label, Object newData) {
    057            /* Handle case where child already exists: */
    058            ExtTree child = (ExtTree)getChild(label);       //@ nowarn Cast;
    059            if (child != null) {
    060                return child;
    061            }
    062
    063            child = new ExtTree(this, label, newData);
    064            edges.put(label, child);
    065            return child;
    066        }
    067
    068
    069        /**
    070         * This is an extended version of addChild that takes a path (a
    071         * list of labels) instead of a single label.  It returns the child
    072         * located by following path from this node.  It creates any
    073         * necessary nodes along the way using addChild with null for
    074         * newData.  Path must be non-null.
    075         */
    076        /*@ requires path != null &&
    077            (\forall int i; (0<=i && i<path.length) ==> path[i] != null); */
    078        //@ ensures \result != null;
    079        public ExtTree addPath(String[] path) {
    080            ExtTree currentNode = this;
    081
    082            for (int i=0; i<path.length; i++)
    083                currentNode = currentNode.addChild(path[i], null);
    084
    085            return currentNode;
    086        }
    087    }