001    /* Copyright 2000, 2001, Compaq Computer Corporation */
002    
003    package javafe.filespace;
004    
005    
006    import java.io.*;
007    
008    import java.util.Enumeration;
009    import java.util.zip.*;
010    
011    import javafe.genericfile.*;
012    
013    
014    /**
015     * A ZipTree is a Tree that mirrors the contents of a zipfile;
016     * the constructor takes in a pathname and returns a tree
017     * representing the filesystem contained in that zipfile.<p>
018     *
019     * ZipTree works by scanning the zipfile at object creation time,
020     * building up a hierarchical list of all the files in the zipfile.
021     * Later modifications to the zipfile will not be reflected in the
022     * ZipTree.<p>
023     *
024     * The data field of every (sub)node in a ZipTree contains a
025     * non-null ZipGenericFile representing the file it mirrors (or would
026     * mirror if a corresponding entry existed) in the underlying zipfile.<p>
027     *
028     * 
029     * Note: ZipTree interior or root nodes (and only interior or root
030     * nodes) may contain ZipGenericFiles that do not have a corresponding
031     * zip entry because there may be no zip entries for those directories.
032     * E.g., the zipfile might contain a file for X/Y but not for X<p>
033     *
034     * We use "./" as the ZipGenericFile name to represent the missing
035     * root directory (no ZipTree actually has a root directory as far as
036     * we can tell).
037     *
038     * This gives the right isDirectory behavior (since it ends with a
039     * "/"), but the wrong local name (".").  This is the best we can do,
040     * though, since the other alternative ("") gives the reverse
041     * behavior, which is worse for us since we rely on the isDirectory
042     * bit and only use local names for non-directories.
043     */
044    
045    class ZipTree extends ExtTree {
046    
047        /***************************************************
048         *                                                 *
049         * Creation:                                       *
050         *                                                 *
051         **************************************************/
052    
053        /** The zipfile we are a snapshot of */
054        //@ invariant zip != null;
055        protected ZipFile zip;
056    
057    
058        /**
059         * Initialize a node's data field to a ZipGenericFile that
060         * represents the file that it would correspond to if the tree it
061         * belongs to mirrored zip.<p>
062         */
063        //@ requires node != null && zip != null;
064        protected static void missingEntry(Tree node, ZipFile zip) {
065            String name = node.getLabel();
066            if (name==null)
067                name = "./";
068    
069            for (Tree ptr = node.getParent(); ptr != null; ptr=ptr.getParent()) {
070                if (ptr.getLabel() != null)
071                    name = ptr.getLabel() + "/" + name;
072            }
073            
074            node.data = new ZipGenericFile(zip, new ZipEntry(name));
075        }
076    
077    
078        /**
079         * Create a ZipTree to mirror a zipfile's contents.<p>
080         *
081         * May throw an IOException (e.g., file doesn't exist) or a
082         * ZipException (e.g., file is not a properly formatted
083         * zipfile).
084         **/
085        public ZipTree(/*@ non_null @*/ File zipfile) throws IOException, ZipException {
086            super(null);
087    
088            // Open the file as a ZipFile:
089            zip = new ZipFile(zipfile);
090    
091            // Then initialize us using the ZipFile's table of contents:
092            loadZipData();
093        }
094    
095        /**
096         * Create a tree of ZipEntry's from the pathnames of the ZipEntry's
097         * in zip
098         */
099        private void loadZipData() {
100            // data may be overwritten later if an entry exists for us:
101            missingEntry(this, zip);                
102    
103            for (Enumeration E=zip.entries(); E.hasMoreElements(); ) {
104                ZipEntry next = (ZipEntry)E.nextElement();
105                addZipEntry(next);
106            }
107        }
108    
109        /** Add a ZipEntry to this tree according to its pathname: */
110        //@ requires z != null;
111        private void addZipEntry(ZipEntry z) {
112            String pathname = z.getName();
113    
114    //      System.out.println("entry: " + pathname + (z.isDirectory()?" D":""));
115    
116            //
117            // Note: ZipEntry's always use '/' as their separator!
118            //
119    
120            // Strip off any leading file separators:
121            while (pathname.length()>0 && pathname.charAt(0)=='/')
122                pathname = pathname.substring(1);
123    
124            // Strip off any trailing file separators:
125            while (pathname.length()>0 &&
126                    pathname.charAt(pathname.length()-1)=='/')
127                pathname = pathname.substring(0,pathname.length()-1);
128    
129            // Locate/create a node corresponding to path:
130            String[] path = StringUtil.parseList(pathname, '/');
131            Tree fileNode = addPath(path);
132    
133            fileNode.data = new ZipGenericFile(zip, z);
134    
135            // Initialize any new interior nodes as missing entries;
136            for (; fileNode != null; fileNode = fileNode.getParent())
137                if (fileNode.data==null)
138                    missingEntry(fileNode, zip);
139        }
140    
141    
142        /***************************************************
143         *                                                 *
144         * Debugging functions:                            *
145         *                                                 *
146         **************************************************/
147    
148        /** A simple test driver */
149        //@ requires args != null;
150        /*@ requires (\forall int i; (0<=i && i<=args.length)
151                    ==> args[i] != null); */
152        public static void main(String[] args) {
153            if (args.length != 1) {
154                System.out.println("ZipTree: usage <zipfile>");
155                return;
156            }
157    
158            /*
159             * Create a new ZipTree from the file args[0] and then 
160             * print it out.
161             */
162            try {
163                Tree T = new ZipTree(new File(args[0]));
164    //          T.print("");
165    
166                // Enumerate its subtrees:
167                for (Enumeration E = new TreeWalker(T);
168                    E.hasMoreElements();) {
169                    Tree subtree = (Tree)E.nextElement();
170                    if (subtree.getChildrenCount() == 0) {
171                        System.out.println("  " + subtree.getLabel());
172                    } else
173                        System.out.println(subtree.getQualifiedName(".") + ":");
174    
175                    /*
176                    System.out.println("[local name = "
177                                +((GenericFile)subtree.data).getLocalName()+"]");
178                    System.out.println("[entry name = "
179                                +((GenericFile)subtree.data).getHumanName()+"]");
180                    */
181                }
182    
183            } catch (Exception E) {
184                System.out.println("Caught " + E);
185            };
186    
187        }
188    }