Index: dart/editor/tools/plugins/com.google.dart.tools.debug.core/src/com/google/dart/tools/debug/core/webkit/WebkitPropertyDescriptor.java |
=================================================================== |
--- dart/editor/tools/plugins/com.google.dart.tools.debug.core/src/com/google/dart/tools/debug/core/webkit/WebkitPropertyDescriptor.java (revision 37110) |
+++ dart/editor/tools/plugins/com.google.dart.tools.debug.core/src/com/google/dart/tools/debug/core/webkit/WebkitPropertyDescriptor.java (working copy) |
@@ -128,7 +128,19 @@ |
@Override |
public int compareTo(WebkitPropertyDescriptor other) { |
- return getName().toUpperCase().compareTo(other.getName().toUpperCase()); |
+ String name0 = getName(); |
+ String name1 = other.getName(); |
+ |
+ // Special case names starting with `[[` (like [[class]]). |
+ if (name0.startsWith("[[")) { |
+ name0 = "~" + name0; |
+ } |
+ |
+ if (name1.startsWith("[[")) { |
+ name1 = "~" + name1; |
+ } |
+ |
+ return name0.compareToIgnoreCase(name1); |
} |
/** |