private class MInterval
{
- // Start and end positions of the MText covered of this interval
- // and its children. The values are actually (4N +- 1), where N
- // is a non-negative integer representing a position relative to
- // the parent interval.
+ // Start and end positions of this interval and its children.
+ // If this is the left node, the values are relative to the
+ // parent's total_start. Otherwise, the values are relatie to
+ // the parent's total_end.
private int total_start, total_end;
// Stack of MTextProperty
private Stack<MTextProperty> stack;
- // Number of child nodes
- private int nodes;
+ private int depth;
private MInterval left, right, parent;
+ public MInterval (int start, bool front_inclusive,
+ int end, bool rear_inclusive)
+ {
+ if (start > end)
+ throw new Exception ("Invalid Interval Range");
+ this.total_start = (start << 2) + (front_inclusive ? -1 : 1);
+ this.total_end = (end << 2) + (rear_inclusive ? 1 : -1);
+ this.stack = new Stack<MTextProperty> ();
+ this.depth = 1;
+ }
+
+ private MInterval (int start, int end, Stack<MTextProperty> stack)
+ {
+ this.total_start = start;
+ this.total_end = end;
+ this.stack = new Stack<MTextProperty> (stack);
+ this.depth = 1;
+ }
+
+ private MInterval Copy ()
+ {
+ return new MInterval (total_start, total_end, stack);
+ }
+
private int Start {
get {
return (left == null ? total_start : total_start + left.total_end);
private int End {
get {
- return (right == null ? total_end : total_start + right.total_start);
+ return (right == null ? total_end : total_end + right.total_start);
}
}
MInterval interval;
if (left != null)
- {
- for (interval = left; interval.right != null;
- interval = interval.right);
- }
+ for (interval = left;
+ interval.right != null;
+ interval = interval.right);
else
- {
- for (interval = parent;
- interval != null && interval.total_start == total_start;
- interval = interval.parent);
- }
+ for (interval = parent;
+ interval != null && interval.total_start == 0;
+ interval = interval.parent);
+
return interval;
}
}
MInterval interval;
if (right != null)
- {
- for (interval = right; interval.left != null;
- interval = interval.left);
- }
+ for (interval = right;
+ interval.left != null;
+ interval = interval.left);
else
- {
- for (interval = parent;
- interval != null && interval.total_end == total_end;
- interval = interval.parent);
- }
+ for (interval = parent;
+ interval != null && interval.total_start < 0;
+ interval = interval.parent);
+
return interval;
}
}
- private static int MakePosition (int pos, bool front_inclusive)
- {
- return (pos << 2) + (front_inclusive ? -1 : 1);
- }
-
- private MInterval (int start, int end)
- {
- if (start > end)
- throw new Exception ("Invalid Interval Range");
- this.total_start = (start << 2) + 1;
- this.total_end = (end << 2) + -1;
- this.stack = new Stack<MTextProperty> ();
- this.nodes = 1;
- }
-
- public MInterval (int start, bool front_inclusive,
- int end, bool rear_inclusive)
- {
- if (start > end)
- throw new Exception ("Invalid Interval Range");
- this.total_start = (start << 2) + (front_inclusive ? -1 : 1);
- this.total_end = (end << 2) + (rear_inclusive ? 1 : -1);
- this.stack = new Stack<MTextProperty> ();
- this.nodes = 1;
- }
-
public void Push (MTextProperty prop, int start, int end)
{
start <<= 2;
private MInterval divide_right (int pos)
{
- MInterval interval = new MInterval (pos, End);
+ MInterval interval = Copy ();
+ int this_start = Start;
+ int this_end = End;
+
+ if (left == null || (right != null && left.depth < right.depth))
+ {
+ interval.left = this;
+ interval.right = right;
+ interval.parent = parent;
+ if (parent != null)
+ {
+ if (total_start == 0)
+ parent.left = interval;
+ else
+ parent.right = interval;
+ }
+ interval.depth = depth;
+ if (right == null)
+ interval.depth++;
+ total_start = 0;
+ total_end = pos - this_start;
+ }
+ else
+ {
+ interval.total_start = pos - this_end;
+ interval.total_end = 0;
+ if (right != null)
+ right.parent = interval;
+ right = interval;
+ }
return interval;
}
private MInterval divide_left (int pos)
{
- MInterval interval = new MInterval (Start, pos);
+ MInterval interval = Copy ();
+ int this_start = Start;
+ int this_end = End;
+
+ if (left == null || (right != null && left.depth < right.depth))
+ {
+ interval.total_start = 0;
+ interval.total_end = pos - this_start;
+ if (left != null)
+ left.parent = interval;
+ left = interval;
+ }
+ else
+ {
+ interval.right = this;
+ interval.left = left;
+ interval.parent = parent;
+ if (parent != null)
+ {
+ if (total_start == 0)
+ parent.left = interval;
+ else
+ parent.right = interval;
+ }
+ interval.depth = depth;
+ if (left == null)
+ interval.depth++;
+ total_start = pos - this_end;
+ total_end = 0;
+ }
return interval;
}