    001    /* Copyright 2000, 2001, Compaq Computer Corporation */
    002
    003    package javafe.filespace;
    004
    005
    006    import java.util.Enumeration;
    007
    008
    009    /**
    010     * A LeafTree is a degenerate form of Tree that never contains
    011     * children.  It is used for the leaf nodes of a Tree.
    012     */
    013
    014    class LeafTree extends Tree {
    015
    016        /***************************************************
    017         *                                                 *
    018         * Creation:                                       *
    019         *                                                 *
    020         **************************************************/
    021
    022        /** Create a root node: */
    023        public LeafTree(Object data) {
    024            super(data);
    025        }
    026
    027        /** Create a non-root node: */
    028        //@ requires parent != null && label != null;
    029        /* package */ LeafTree(Tree parent, String label, Object data) {
    030            super(parent, label, data);
    031        }
    032
    033
    034        /***************************************************
    035         *                                                 *
    036         * Fetching and counting children:                 *
    037         *                                                 *
    038         **************************************************/
    039
    040        /*
    041         * Hardwire the fact that we never have children.  New definitions
    042         * of isLeaf and getChildrenCount are provided for efficiency
    043         * reasons.
    044         */
    045
    046        public final Enumeration children() {
    047            Enumeration empty = new EmptyEnum();
    048            //@ set empty.elementType = \type(Tree);
    049
    050            return empty;
    051        }
    052
    053        public final boolean isLeaf() {
    054            return true;
    055        }
    056
    057        public final int getChildrenCount() {
    058            return 0;
    059        }
    060    }