// ResourceSpaceManager.java
// $Id: ResourceSpaceManager.java,v 1.4 1997/07/30 14:03:55 ylafon Exp $  
// (c) COPYRIGHT MIT and INRIA, 1997.
// Please first read the full copyright statement in file COPYRIGHT.html

package w3c.tools.resources;

import java.io.*;
import java.util.*;

public class ResourceSpaceManager {
  // THE resource space manager
  private static ResourceSpaceManager theManager = null;

  /**
   * Properties - The config directory for spaces.
   */
  public static final
  String CONFIGDIR_P = "w3c.tools.resources.space.config";
  /**
   * Properties - The class name for a given space.
   */
  public static final 
  String CLASSNAME_P = "w3c.tools.resources.space.class";
    
  /**
   * That space config directory.
   */
  protected File directory = null;
  /**
   * List of loaded resource spaces.
   */
  protected Hashtable spaces = null;
    
  /**
   * Get the space manager for that application.
   * @return The singleton ResourceSpaceManager instance.
   */

  public static synchronized ResourceSpaceManager getResourceSpaceManager() {
    if ( theManager == null ) {
      Properties p = System.getProperties();
      File       f = new File((String) p.get(CONFIGDIR_P));
      theManager   = new ResourceSpaceManager(f);
    }
    return theManager;
  }

  /**
   * Get a resource space.
   * @param name The name of that resource space.
   */

  public synchronized ResourceSpace getResourceSpace(String name) 
    throws ResourceSpaceInitException
  {
    // Is this space already loaded ?
    ResourceSpace space = (ResourceSpace) spaces.get(name);
    if ( space != null )
      return space;
    // Load that space:
    String className = null;
    File   propFile  = new File(directory, name+".sp");
    try {
      // Initialize the properties set:
      Properties p = (Properties) System.getProperties().clone();
      p.load(new BufferedInputStream(new FileInputStream(propFile)));
      // Get the class for the space, instantiate and init:
      className = (String) p.get(CLASSNAME_P);
      if ( className == null )
	throw new ResourceSpaceInitException("no class property for \""+
					     name+
					     "\" space.");
      space = ((ResourceSpace) Class.forName(className).newInstance());
      space.init(p, null);
      // Register that space:
      spaces.put(name, space);
    } catch (ResourceSaverInitException ex) {
      throw new ResourceSpaceInitException("Saver : "+ex.getMessage());
    } catch (ClassNotFoundException ex) {
      // Unable to find the space class
      throw new ResourceSpaceInitException("unable to find space \""+
					   name
					   + "\" class: "+
					   className);
    } catch (InstantiationException ex) {
      // Unable to instantiate space class:
      throw new ResourceSpaceInitException("unable to instantiate class "+
					   className
					   + " of space \""+
					   name +"\"");
    } catch (IllegalAccessException ex) {
      // Unable to instantiate the space class
      throw new ResourceSpaceInitException("unable to access class "+
					   className
					   + " of space \""+
					   name +"\"");
    } catch (IOException ex) {
      // Unable to load property file:
      throw new ResourceSpaceInitException("unable to load properties \""+
					   propFile
					   + "\" "+ex.getMessage());
    } 
    return space;
  }

  /**
   * Create and initialize a manager for the given directory of spaces.
   * @param dir The config directory for that resource space manager.
   */

  private ResourceSpaceManager(File dir) {
    this.directory = dir;
    this.spaces    = new Hashtable(11);
  }
    
	
}
