Version 1.5.0-dev.4.5

dart/editor/tools/plugins/com.google.dart.tools.debug.core/src/com/google/dart/tools/debug/core/webkit/WebkitPropertyDescriptor.java

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);
   }
 
   /**