| Index: dart/editor/tools/plugins/com.google.dart.tools.core/src/com/google/dart/tools/core/internal/builder/IgnoreResourceFilter.java
|
| ===================================================================
|
| --- dart/editor/tools/plugins/com.google.dart.tools.core/src/com/google/dart/tools/core/internal/builder/IgnoreResourceFilter.java (revision 34682)
|
| +++ dart/editor/tools/plugins/com.google.dart.tools.core/src/com/google/dart/tools/core/internal/builder/IgnoreResourceFilter.java (working copy)
|
| @@ -16,6 +16,8 @@
|
| import com.google.dart.tools.core.DartCore;
|
| import com.google.dart.tools.core.internal.model.DartIgnoreManager;
|
|
|
| +import org.eclipse.core.resources.IResource;
|
| +
|
| /**
|
| * A delta listener that filters out sources specified by {@link DartIgnoreManager} and broadcasts
|
| * any remaining changes to its own listeners. For performance, this filter caches information about
|
| @@ -128,6 +130,12 @@
|
| * @return {@code true} if the event should be forwarded
|
| */
|
| private boolean shouldForward(ResourceDeltaEvent event) {
|
| - return !hasIgnores || ignoreManager.isAnalyzed(event.getResource().getLocation());
|
| + if (hasIgnores) {
|
| + IResource res = event.getResource();
|
| + if (res == null || ignoreManager.isIgnored(res.getLocation())) {
|
| + return false;
|
| + }
|
| + }
|
| + return true;
|
| }
|
| }
|
|
|