private int cached_index = -1;
private int cached_slot = -1;
+
+ private FinalizationHelper fh;
// Public API //////////////////////////////////////////////////////////////////////////
if (root != 0) {
insert(index, arg, root, 0, false, false);
} else {
+ if(fh == null) fh = new FinalizationHelper(this);
root = arg;
left[arg] = right[arg] = parent[arg] = 0;
size[arg] = 1;
root = 0;
}
}
-
- protected void finalize() { clear(); }
-
// Node Data /////////////////////////////////////////////////////////////////////////
return slot;
}
}
+
+ static class FinalizationHelper {
+ private BalancedTree bt;
+ FinalizationHelper(BalancedTree bt) { this.bt = bt; }
+ protected void finalize() { bt.clear(); }
+ }
// Debugging ///////////////////////////////////////////////////////////////////////////