platform/org.eclipse.core.resources/src/org/eclipse/core/resources/ResourcesPlugin.java
changeset 16 06d88bb6aac0
parent 12 063eb66097dc
--- a/platform/org.eclipse.core.resources/src/org/eclipse/core/resources/ResourcesPlugin.java	Mon Jun 01 19:29:06 2009 -0500
+++ b/platform/org.eclipse.core.resources/src/org/eclipse/core/resources/ResourcesPlugin.java	Tue Jun 02 09:59:27 2009 -0500
@@ -18,6 +18,8 @@
 import org.osgi.framework.BundleActivator;
 import org.osgi.framework.BundleContext;
 
+import java.util.logging.Level;
+
 /**
  * The plug-in runtime class for the Resources plug-in.  This is
  * the starting point for all workspace and resource manipulation.
@@ -29,6 +31,7 @@
  * @noinstantiate This class is not intended to be instantiated by clients.
  */
 public final class ResourcesPlugin extends Plugin {
+
 	/**
 	 * Unique identifier constant (value <code>"org.eclipse.core.resources"</code>)
 	 * for the standard Resources plug-in.
@@ -267,6 +270,10 @@
 	 */
 	private static Workspace workspace = null;
 
+	
+	private static final String REFRESH_LOG_ID = ".refresh.log";
+	private DiagnosticLog refreshLog;
+	
 	/** 
 	 * Constructs an instance of this plug-in runtime class.
 	 * <p>
@@ -377,4 +384,18 @@
 		if (!result.isOK())
 			getLog().log(result);
 	}
+	
+	public static void writeRefreshLog(String s) {
+		if (!plugin.getPluginPreferences().getBoolean(PI_RESOURCES + REFRESH_LOG_ID))
+			return;
+		
+		if (plugin.refreshLog == null) {
+			IPath path = getWorkspace().getRoot().getLocation().append("refresh.log");
+			plugin.refreshLog = new DiagnosticLog("refresh.log", PI_RESOURCES + REFRESH_LOG_ID, path.toOSString());
+			plugin.refreshLog.getLogger().setLevel(Level.INFO);
+		}
+
+		plugin.refreshLog.getLogger().info(s);
+		System.out.println(s);
+	}
 }