// Copyright (c) 2003 Compaq Corporation.  All rights reserved.
// Portions Copyright (c) 2003 Microsoft Corporation.  All rights reserved.
// Last modified on Mon 30 Apr 2007 at 13:18:28 PST by lamport
//      modified on Mon Jan 29 16:21:11 PST 2001 by yuanyu

package tlc2.tool;

import java.io.File;
import java.net.URL;
import java.net.URLClassLoader;

import tlc2.output.EC;
import util.Assert;
import util.FilenameToStream;

/**
 * 
 * @author Yuan Yu, Simon Zambrovski
 * @version $Id$
 */
public class TLAClass
{
    /* Load a class from a file. */
    private final String pkg;
	private final FilenameToStream resolver;

    public TLAClass(String pkg, FilenameToStream resolver)
    {
        this.resolver = resolver;
		if (pkg.length() != 0 && pkg.charAt(pkg.length() - 1) != '.')
        {
            this.pkg = pkg + '.';
        } else
        {
            this.pkg = pkg;
        }
    }

    /**
     * This method attempts to load the java class with the given name.
     **/
    public synchronized Class loadClass(String name)
    {
        Class cl = null;
        try
        {
        	try {
    			final File module = resolver.resolve(name + ".class", false);
    			if (module != null && module.getAbsoluteFile() != null) {
    				final URL url = module.getAbsoluteFile().getParentFile().toURI().toURL();
					cl = new URLClassLoader(new URL[] {url}).loadClass(name);
    			}
        	} catch (Exception ignored1) {
        		/*SKIP*/
        	} finally {
        		if (cl == null) {
        			try
        			{
        				cl = Class.forName(name);
        			} catch (Exception e)
        			{ /*SKIP*/
        			}
        		}
        	}
            if (cl == null)
            {
                try
                {
                    cl = Class.forName(this.pkg + name);
                } catch (Exception e)
                { /*SKIP*/
                }
            }
        } catch (Throwable e)
        {
            Assert.fail(EC.TLC_ERROR_REPLACING_MODULES, new String[] { name, 
                       (e.getMessage()==null)?e.toString():e.getMessage() });
        }
        return cl;
    }
    
//
//    public static void main(String argv[])
//    {
//        TLAClass tc = new TLAClass("tlc2.module");
//        Class c = tc.loadClass("Strings"); // must set CLASSPATH correctly
//        System.err.println("c = " + c);
//        // Class c1 = tc.loadClass("Class");
//        // System.err.println("c1 = " + c1);
//    }
//
}

@@ -905,20 +905,14 @@
  %7D%0A%0A
-    /**%0A    
+%09/**%0A%09
  * T
@@ -975,20 +975,662 @@
 n name.%0A
-    
+%09 * %0A%09 * Loading classes is done in three steps:%0A%09 * %0A%09 * %3Cul%3E%0A%09 * %3Cli%3E1) TLC's %7B@link FilenameToStream%7D resolver is used to locate a class%0A%09 * file in the resolver's lookup path. Check %7B@link FilenameToStream%7D's%0A%09 * documentation on the lookup order. If a class file with name %22name.class%22%0A%09 * can be found, it is loaded.%3C/li%3E%0A%09 * %3Cli%3E2) With the unqualified name, we try to lookup the class in the%0A%09 * regular VM's CLASSPATH.%3C/li%3E%0A%09 * %3Cli%3E3) As a last resort, we try to load a class fully qualified with the%0A%09 * package name given in %7B@link TLAClass#pkg%7D.%3C/li%3E%0A%09 * %3C/ul%3E%0A%09 * %3Cp%3E%0A%09 * If no class could be loaded, %3Ccode%3Enull%3C/code%3E is returned.%0A%09
  **/%0A   

Add documentation in which order classloading attempts are carried out.