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    }