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 }