    001    /* Copyright 2000, 2001, Compaq Computer Corporation */
    002
    003    package javafe.filespace;
    004
    005
    006    import java.util.Enumeration;
    007
    008    /**
    009     * A FilterEnum filters an underlying Enumeration using a client
    010     * supplied Filter.
    011     */
    012
    013
    014    class FilterEnum extends LookAheadEnum {
    015
    016        /** The underlying Enumeration: */
    017        //@ invariant underlyingEnum != null;
    018        //@ invariant !underlyingEnum.returnsNull;
    019        //@ invariant underlyingEnum.owner == this;
    020        protected Enumeration underlyingEnum;
    021
    022        // We inherit our properties from the underlying Enumeration:
    023        //@ invariant elementType == underlyingEnum.elementType;
    024
    025
    026        /** The filter we are using: */
    027        //@ invariant filter != null;
    028        //@ invariant filter.acceptedType == elementType;
    029        public Filter filter;
    030
    031
    032        /***************************************************
    033         *                                                 *
    034         * Creation:                                       *
    035         *                                                 *
    036         **************************************************/
    037
    038        /**
    039         * Filter the Enumeration E using Filter F:
    040         */
    041        //@ requires E != null && F != null;
    042        //@ requires !E.returnsNull;
    043        //@ requires E.owner == null;
    044        //@ requires E.elementType == F.acceptedType;
    045        //@ ensures elementType == E.elementType;
    046        public FilterEnum(Enumeration E, Filter F) {
    047            super();
    048
    049            //@ set E.owner = this;
    050            underlyingEnum = E;
    051            filter = F;
    052
    053            //@ set elementType = E.elementType;
    054        }
    055
    056
    057        /***************************************************
    058         *                                                 *
    059         * Calculating the next element:                   *
    060         *                                                 *
    061         **************************************************/
    062
    063        /**
    064         * Compute the next element in the series, or return null if the
    065         * series is exhausted.
    066         */
    067
    068        protected Object calcNextElement() {
    069            while (underlyingEnum.hasMoreElements()) {
    070                Object next = underlyingEnum.nextElement();
    071
    072                if (filter.accept(next))
    073                    return next;
    074            }
    075
    076            return null;
    077        }
    078    }