Compressed/optimized navigation notification.

editor/tools/plugins/com.google.dart.server/src/com/google/dart/server/generated/types/NavigationRegion.java

Index: editor/tools/plugins/com.google.dart.server/src/com/google/dart/server/generated/types/NavigationRegion.java
diff --git a/editor/tools/plugins/com.google.dart.server/src/com/google/dart/server/generated/types/NavigationRegion.java b/editor/tools/plugins/com.google.dart.server/src/com/google/dart/server/generated/types/NavigationRegion.java
index 8da8dbafe01681c939c221db98da99c1250999fb..6ec27604d9d613b3320cea4150144284b6e31137 100644
--- a/editor/tools/plugins/com.google.dart.server/src/com/google/dart/server/generated/types/NavigationRegion.java
+++ b/editor/tools/plugins/com.google.dart.server/src/com/google/dart/server/generated/types/NavigationRegion.java
@@ -54,18 +54,20 @@ public class NavigationRegion {
   private final int length;
 
   /**
-   * The elements to which the given region is bound. By opening the declaration of the elements,
-   * clients can implement one form of navigation.
+   * The indexes of the targets (in the enclosing navigation response) to which the given region is
+   * bound. By opening the target, clients can implement one form of navigation.
    */
-  private final List<Element> targets;
+  private final int[] targetIndexes;
+
+  private List<NavigationTarget> allTargets;
 
   /**
    * Constructor for {@link NavigationRegion}.
    */
-  public NavigationRegion(int offset, int length, List<Element> targets) {
+  public NavigationRegion(int offset, int length, int[] targetIndexes) {
     this.offset = offset;
     this.length = length;
-    this.targets = targets;
+    this.targetIndexes = targetIndexes;
   }
 
   public boolean containsInclusive(int x) {
@@ -79,7 +81,7 @@ public class NavigationRegion {
       return
         other.offset == offset &&
         other.length == length &&
-        ObjectUtilities.equals(other.targets, targets);
+        Arrays.equals(other.targetIndexes, targetIndexes);
     }
     return false;
   }
@@ -87,8 +89,8 @@ public class NavigationRegion {
   public static NavigationRegion fromJson(JsonObject jsonObject) {
     int offset = jsonObject.get("offset").getAsInt();
     int length = jsonObject.get("length").getAsInt();
-    List<Element> targets = Element.fromJsonArray(jsonObject.get("targets").getAsJsonArray());
-    return new NavigationRegion(offset, length, targets);
+    int[] targetIndexes = JsonUtilities.decodeIntArray(jsonObject.get("targetIndexes").getAsJsonArray());
+    return new NavigationRegion(offset, length, targetIndexes);
   }
 
   public static List<NavigationRegion> fromJsonArray(JsonArray jsonArray) {
@@ -103,6 +105,16 @@ public class NavigationRegion {
     return list;
   }
 
+  public List<NavigationTarget> getTargets() {
+    List<NavigationTarget> targets = new ArrayList<NavigationTarget>();
+    for (int i = 0; i < targetIndexes.length; i++) {
+      int targetIndex = targetIndexes[i];
+      NavigationTarget target = allTargets.get(targetIndex);
+      targets.add(target);
+    }
+    return targets;
+  }
+
   /**
    * The length of the region from which the user can navigate.
    */
@@ -118,11 +130,11 @@ public class NavigationRegion {
   }
 
   /**
-   * The elements to which the given region is bound. By opening the declaration of the elements,
-   * clients can implement one form of navigation.
+   * The indexes of the targets (in the enclosing navigation response) to which the given region is
+   * bound. By opening the target, clients can implement one form of navigation.
    */
-  public List<Element> getTargets() {
-    return targets;
+  public int[] getTargetIndexes() {
+    return targetIndexes;
   }
 
   @Override
@@ -130,19 +142,23 @@ public class NavigationRegion {
     HashCodeBuilder builder = new HashCodeBuilder();
     builder.append(offset);
     builder.append(length);
-    builder.append(targets);
+    builder.append(targetIndexes);
     return builder.toHashCode();
   }
 
+  public void setAllTargets(List<NavigationTarget> allTargets) {
+    this.allTargets = allTargets;
+  }
+
   public JsonObject toJson() {
     JsonObject jsonObject = new JsonObject();
     jsonObject.addProperty("offset", offset);
     jsonObject.addProperty("length", length);
-    JsonArray jsonArrayTargets = new JsonArray();
-    for (Element elt : targets) {
-      jsonArrayTargets.add(elt.toJson());
+    JsonArray jsonArrayTargetIndexes = new JsonArray();
+    for (int elt : targetIndexes) {
+      jsonArrayTargetIndexes.add(new JsonPrimitive(elt));
     }
-    jsonObject.add("targets", jsonArrayTargets);
+    jsonObject.add("targetIndexes", jsonArrayTargetIndexes);
     return jsonObject;
   }
 
@@ -154,8 +170,8 @@ public class NavigationRegion {
     builder.append(offset + ", ");
     builder.append("length=");
     builder.append(length + ", ");
-    builder.append("targets=");
-    builder.append(StringUtils.join(targets, ", "));
+    builder.append("targetIndexes=");
+    builder.append(StringUtils.join(targetIndexes, ", "));
     builder.append("]");
     return builder.toString();
   }