MText.cs

   1 using System;
   2 using System.Text;
   3 using System.Collections;
   4 using System.Collections.Generic;
   5 using M17N.Core;
   6
   7 namespace M17N.Core
   8 {
   9 #if false
  10   public enum MTextFormat
  11     {
  12       MTEXT_FORMAT_US_ASCII,
  13       MTEXT_FORMAT_UTF_8,
  14       MTEXT_FORMAT_UTF_16BE,
  15       MTEXT_FORMAT_UTF_16LE,
  16       MTEXT_FORMAT_UTF_32BE,
  17       MTEXT_FORMAT_UTF_32LE,
  18     }
  19 #endif
  20
  21   public class MTextProperty
  22   {
  23     internal MSymbol key;
  24     internal object val;
  25
  26     [FlagsAttribute]
  27     internal enum Flag : byte
  28       {
  29         None =          0,
  30         FrontSticky =   1,
  31         RearSticky =    2,
  32         Sensitive =     4
  33       };
  34     internal Flag flags;
  35
  36     public MSymbol Key { get { return key; } }
  37     public object Val { get { return val; } }
  38     public bool FrontSticky
  39     {
  40       get { return (flags & Flag.FrontSticky) != Flag.None; }
  41     }
  42     public bool RearSticky
  43     {
  44       get { return (flags & Flag.RearSticky) != Flag.None; }
  45     }
  46     public bool Sensitive
  47     {
  48       get { return (flags & Flag.Sensitive) != Flag.None; }
  49     }
  50
  51     public MTextProperty (MSymbol key, object val)
  52     {
  53       this.key = key;
  54       this.val = val;
  55       flags |= Flag.RearSticky;
  56     }
  57
  58     public MTextProperty (MSymbol key, object val,
  59                           bool front_sticky, bool rear_sticky, bool sensitive)
  60     {
  61       this.key = key;
  62       this.val = val;
  63       if (front_sticky)
  64         flags |= Flag.FrontSticky;
  65       if (rear_sticky)
  66         flags |= Flag.RearSticky;
  67       if (sensitive)
  68         flags |= Flag.Sensitive;
  69     }
  70   }
  71
  72   public class MText : IEnumerable, IEquatable<MText>, IComparable<MText>
  73   {
  74 #if false
  75     public enum MTextFormat format;
  76 #endif
  77     private StringBuilder sb;
  78     private int nchars;
  79     private int cache_pos;
  80     private int cache_idx;
  81     private MPlist intervals;
  82     private MPlist default_property;
  83     private bool read_only;
  84
  85     private static UTF8Encoding utf8 = new UTF8Encoding ();
  86
  87     private static int count_chars (String str)
  88     {
  89       int len = str.Length, n = 0;
  90
  91       for (int i = 0; i < len; i++, n++)
  92         if (surrogate_high_p (str[i]))
  93           i++;
  94       return n;
  95     }
  96
  97     private static int count_chars (StringBuilder str)
  98     {
  99       int len = str.Length, n = 0;
 100
 101       for (int i = 0; i < len; i++, n++)
 102         if (surrogate_high_p (str[i]))
 103           i++;
 104       return n;
 105     }
 106
 107     public MText ()
 108       {
 109         sb = new StringBuilder ();
 110         intervals = new MPlist ();
 111       }
 112
 113     public MText (byte[] str)
 114       {
 115         sb = new StringBuilder (utf8.GetString (str));
 116         nchars = count_chars (sb);
 117         intervals = new MPlist ();
 118       }
 119
 120     public MText (String str)
 121       {
 122         sb = new StringBuilder (str);
 123         nchars = count_chars (str);
 124         intervals = new MPlist ();
 125       }
 126
 127     public MText (StringBuilder str)
 128       {
 129         sb = str;
 130         nchars = count_chars (str);
 131         intervals = new MPlist ();
 132       }
 133
 134     public static MText operator+ (MText mt1, MText mt2)
 135     {
 136       MText mt = new MText ();
 137
 138       mt.sb.Append (mt1.sb);
 139       mt.sb.Append (mt2.sb);
 140       mt.nchars = mt1.nchars + mt2.nchars;
 141       return mt;
 142     }
 143
 144     // Public properties
 145     public bool ReadOnly { get { return read_only; } }
 146     public int Length { get { return nchars; } }
 147
 148     // Public methods
 149
 150     // for IEnumerable interface
 151     public IEnumerator GetEnumerator() { return new MTextEnum (this); }
 152
 153     // for IEquatable interface
 154     public bool Equals (MText other) { return this.sb.Equals (other.sb); }
 155
 156     // for IComparable interface
 157     public int CompareTo (MText other)
 158     {
 159       return this.sb.ToString ().CompareTo (other.sb.ToString ());
 160     }
 161
 162     public override String ToString () { return "\"" + sb.ToString () + "\""; }
 163
 164     private static bool surrogate_high_p (char c)
 165     {
 166       return (c >= 0xD800 && c < 0xDC00);
 167     }
 168
 169     private static bool surrogate_low_p (char c)
 170     {
 171       return (c >= 0xDC00 && c < 0xE000);
 172     }
 173
 174     private static int inc_idx (StringBuilder sb, int i)
 175     {
 176       return (i + (surrogate_high_p (sb[i]) ? 2 : 1));
 177     }
 178
 179     private static int dec_idx (StringBuilder sb, int i)
 180     {
 181       return (i - (surrogate_low_p (sb[i - 1]) ? 2 : 1));
 182     }
 183
 184     private static int pos_to_idx (MText mt, int pos)
 185     {
 186       if (pos == mt.cache_pos)
 187         return mt.cache_idx;
 188
 189       int p, i;
 190       bool forward;
 191
 192       if (pos < mt.cache_pos)
 193         {
 194           if (mt.cache_pos == mt.cache_idx)
 195             return mt.cache_idx;
 196           if (pos < mt.cache_pos - pos)
 197             {
 198               p = i = 0;
 199               forward = true;
 200             }
 201           else
 202             {
 203               p = mt.cache_pos; i = mt.cache_idx;
 204               forward = false;
 205             }
 206         }
 207       else
 208         {
 209           if (mt.nchars - mt.cache_pos == mt.sb.Length - mt.cache_idx)
 210             return (mt.cache_idx + pos - mt.cache_pos);
 211           if (pos - mt.cache_pos < mt.nchars - pos)
 212             {
 213               p = mt.cache_pos; i = mt.cache_idx;
 214               forward = true;
 215             }
 216           else
 217             {
 218               p = mt.nchars; i = mt.sb.Length;
 219               forward = false;
 220             }
 221         }
 222       if (forward)
 223         for (; p < pos; i = inc_idx (mt.sb, i), p++);
 224       else
 225         for (; p > pos; i = dec_idx (mt.sb, i), p--);
 226       mt.cache_pos = p;
 227       mt.cache_idx = i;
 228       return i;
 229     }
 230
 231     private void insert (int pos, MText mt2, int from, int to)
 232     {
 233       int pos_idx = pos_to_idx (this, pos);
 234       int from_idx = pos_to_idx (mt2, from);
 235       int to_idx = pos_to_idx (mt2, to);
 236
 237       sb.Insert (pos_idx, mt2.sb.ToString (from_idx, to_idx - from_idx));
 238       nchars += to - from;
 239
 240       foreach (MPlist plist in mt2.intervals)
 241         if (intervals.Find (plist.Key) == null)
 242           intervals.Push (plist.Key, new MInterval (plist.Key, this));
 243       foreach (MPlist plist in intervals)
 244         {
 245           MPlist p = mt2.intervals.Find (plist.Key);
 246           MInterval interval;
 247
 248           if (p.IsEmpty)
 249             interval = new MInterval (plist.Key, to - from);
 250           else
 251             interval = ((MInterval) p.Val).copy (from, to);
 252           ((MInterval) plist.Val).insert (pos, interval);
 253         }
 254     }
 255
 256     public int this[int i]
 257     {
 258       set {
 259         i = pos_to_idx (this, i);
 260         if (value < 0x10000)
 261           {
 262             if (surrogate_high_p (sb[i]))
 263               sb.Remove (i, 1);
 264             sb[i] = (char) value;
 265           }
 266         else
 267           {
 268             char high = (char) (0xD800 + ((value - 0x10000) >> 10));
 269             char low = (char) (0xDC00 + ((value - 0x10000) & 0x3FF));
 270
 271             if (! surrogate_high_p (sb[i]))
 272               sb.Insert (i, 0);
 273             sb[i] = high;
 274             sb[i + 1] = low;
 275           }
 276       }
 277       get {
 278         i = pos_to_idx (this, i);
 279         return (surrogate_high_p (sb[i])
 280                 ? ((sb[i] - 0xD800) << 10) + (sb[i + 1] - 0xDC00) + 0x10000
 281                 : sb[i]);
 282       }
 283     }
 284
 285     public MText Dup ()
 286     {
 287       return (new MText (sb.ToString ()));
 288     }
 289
 290     public MText Ins (int pos, MText mt)
 291     {
 292       insert (pos, mt, 0, mt.nchars);
 293       return this;
 294     }
 295
 296     public MText Ins (int pos, MText mt, int from, int to)
 297     {
 298       insert (pos, mt, from, to);
 299       return this;
 300     }
 301
 302     public MText Del (int from, int to)
 303     {
 304       sb.Remove (from, pos_to_idx (this, to) - pos_to_idx (this, from));
 305       nchars -= to - from;
 306
 307       foreach (MPlist plist in intervals)
 308         ((MInterval) plist.Val).Delete (from, to);
 309       return this;
 310     }
 311
 312     public object GetProp (int pos, MSymbol key)
 313     {
 314       MInterval i = (MInterval) intervals.Find (key).Val;
 315
 316       if (i == null)
 317         return null;
 318
 319       MTextProperty prop = i.Get (pos);
 320       return (prop != null ? prop.Val : null);
 321     }
 322
 323     public object GetProp (int pos, MSymbol key, out MTextProperty prop)
 324     {
 325       MInterval i = (MInterval) intervals.Find (key).Val;
 326
 327       if (i == null)
 328         return (prop = null);
 329       prop = i.Get (pos);
 330       return (prop != null ? prop.Val : null);
 331     }
 332
 333     public object GetProp (int pos, MSymbol key, out MTextProperty[] array)
 334     {
 335       MInterval i = (MInterval) intervals.Find (key).Val;
 336
 337       if (i == null)
 338         return (array = null);
 339       MTextProperty prop = i.Get (pos, out array);
 340       return (prop != null ? prop.Val : null);
 341     }
 342
 343     public void PushProp (int from, int to, MSymbol key, object val)
 344     {
 345       PushProp (from, to, new MTextProperty (key, val));
 346     }
 347
 348     public void PushProp (int from, int to, MTextProperty prop)
 349     {
 350       if (from < 0)
 351         {
 352           if (default_property == null)
 353             default_property = new MPlist ();
 354           default_property.Push (prop.key, prop.val);
 355         }
 356       else
 357         {
 358           MInterval root = (MInterval) intervals.Find (prop.key).Val;
 359
 360           if (root == null)
 361             {
 362               root = new MInterval (prop.key, this);
 363               intervals.Push (prop.key, root);
 364             }
 365           root.Push (from, to, prop);
 366         }
 367     }
 368
 369     public void DumpProp ()
 370     {
 371       foreach (MPlist p in intervals)
 372         ((MInterval) p.Val).Dump ();
 373     }
 374
 375     private class MInterval
 376     {
 377       // position: 0   1   2   3   4   5   6   7
 378       //           | A | B | C | D | E   F | G |
 379       // interval  |---|---|---|<->|-------|---|
 380       //           |---|<->|---|   |<----->|---|
 381       //           |<->|   |<->|           |<->|
 382       //
 383       //                      [7 (3 4)]
 384       //              [3 (1 2)]       [3 (4 6)]
 385       //         [1 (0 1)] [2 (2 3)]      [1 (6 7)]
 386       private int total_length;
 387       private int from, to;
 388       private MSymbol key;
 389       private MPlist stack;
 390       private MInterval left, right, parent;
 391       private MText mtext;
 392
 393       public MInterval (MSymbol key, int length)
 394       {
 395         if (length <= 0)
 396           throw new Exception ("Invalid interval length");
 397         this.key = key;
 398         total_length = length;
 399         stack = new MPlist ();
 400       }
 401
 402       public MInterval (MSymbol key, MText mt)
 403       {
 404         this.key = key;
 405         mtext = mt;
 406         total_length = mt.sb.Length;
 407         from = 0;
 408         to = total_length;
 409         stack = new MPlist ();
 410       }
 411
 412       public MTextProperty Get (int pos)
 413       {
 414         MInterval i = find (pos);
 415
 416         return (i.stack.IsEmpty ? null : (MTextProperty) i.stack.Val);
 417       }
 418
 419       public MTextProperty Get (int pos, out MTextProperty[] array)
 420       {
 421         MInterval i = find (pos);
 422
 423         if (i.stack.IsEmpty)
 424           {
 425             array = null;
 426             return null;
 427           }
 428         array = new MTextProperty[i.stack.Count];
 429
 430         int idx;
 431         MPlist p;
 432         for (idx = 0, p = i.stack; ! p.IsEmpty; idx++, p = p.Next)
 433           array[idx] = (MTextProperty) p.Val;
 434         return array[idx - 1];
 435       }
 436
 437       private MInterval (MSymbol key, int length, MPlist stack)
 438       {
 439         this.key = key;
 440         total_length = length;
 441         from = 0;
 442         to = total_length;
 443         this.stack = stack.Clone ();
 444       }
 445
 446       private void update_from_to ()
 447       {
 448         if (parent != null)
 449           {
 450             from = parent.from - total_length + LeftLength;
 451             to = parent.from - RightLength;
 452           }
 453       }
 454
 455       private int LeftLength
 456       {
 457         get { return (left == null ? 0 : left.total_length); }
 458       }
 459
 460       private int RightLength
 461       {
 462         get { return (right == null ? 0 : right.total_length); }
 463       }
 464
 465       private MInterval left_most_node
 466       {
 467         get { return (left == null ? this : left.left_most_node); }
 468       }
 469
 470       private MInterval right_most_node
 471       {
 472         get { return (right == null ? this : right.right_most_node); }
 473       }
 474
 475       private MInterval prev {
 476         get {
 477           MInterval i;
 478
 479           if (left != null)
 480             for (i = left; i.right != null; i = i.right);
 481           else
 482             for (i = parent; i != null && i.left == null; i = i.parent);
 483           return i;
 484         }
 485       }
 486
 487       private MInterval next {
 488         get {
 489           MInterval i;
 490
 491           if (right != null)
 492             for (i = right; i.left != null; i = i.left);
 493           else
 494             for (i = parent; i != null && i.right == null; i = i.parent);
 495           return i;
 496         }
 497       }
 498
 499       private MInterval find (int pos)
 500       {
 501         update_from_to ();
 502         if (pos < from)
 503           return left.find (pos);
 504         if (pos >= to)
 505           return right.find (pos);
 506         return this;
 507       }
 508
 509       //      p-. or .-p              p-. or .-p
 510       //       .-this-.                .-right-.
 511       //    left   .-right-.  ->   .-this-.    c2
 512       //          c1       c2    left     c1
 513       private MInterval promote_right ()
 514       {
 515         int right_length = right.total_length;
 516         MInterval c1;
 517
 518         if (parent == null)
 519           mtext.intervals.Put (key, right);
 520         else if (parent.left == this)
 521           parent.left = right;
 522         else
 523           parent.right = right;
 524         right.parent = parent;
 525         c1 = right.left;
 526         right.left = this;
 527
 528         parent = right;
 529         right = c1;
 530         parent.total_length += total_length;
 531         total_length -= right_length;
 532         if (c1 != null)
 533           {
 534             c1.parent = this;
 535             parent.total_length -= c1.total_length;
 536             total_length += c1.total_length;
 537           }
 538         return parent;
 539       }
 540
 541       //      p-. or .-p              p-. or .-p
 542       //       .-this-.                .-left-.
 543       //  .-left-.  .-right-.  ->     c1    .-this-.
 544       // c1      c2                        c2     right
 545       private MInterval promote_left ()
 546       {
 547         int left_length = left.total_length;
 548         MInterval c1;
 549
 550         if (parent == null)
 551           mtext.intervals.Put (key, left);
 552         else if (parent.left == this)
 553           parent.left = left;
 554         else
 555           parent.right = left;
 556         left.parent = parent;
 557         c1 = left.left;
 558         left.right = this;
 559
 560         parent = left;
 561         left = c1;
 562         parent.total_length += total_length;
 563         total_length -= left_length;
 564         if (c1 != null)
 565           {
 566             c1.parent = this;
 567             parent.total_length -= c1.total_length;
 568             total_length += c1.total_length;
 569           }
 570         return parent;
 571       }
 572
 573       private MInterval balance ()
 574       {
 575         MInterval i = this;
 576
 577         while (true)
 578           {
 579             //       .-this-.
 580             //  .-left-.  .-right-.
 581             // c1     c2  c3      c4
 582             int diff = i.LeftLength - i.RightLength;
 583             int new_diff;
 584
 585             if (diff > 0)
 586               {
 587                 new_diff = (i.total_length - i.LeftLength
 588                             + i.left.RightLength - i.left.LeftLength);
 589                 if (Math.Abs (new_diff) >= diff)
 590                   break;
 591                 i = i.promote_left ();
 592                 i.right.balance ();
 593               }
 594             else if (diff < 0)
 595               {
 596                 new_diff = (i.total_length - i.RightLength
 597                             + i.right.LeftLength - i.right.RightLength);
 598                 if (Math.Abs (new_diff) >= diff)
 599                   break;
 600                 i = i.promote_right ();
 601                 i.left.balance ();
 602               }
 603           }
 604         return i;
 605       }
 606
 607       public MInterval copy (int start, int end)
 608       {
 609         MInterval this_copy, left_copy = null, right_copy = null;
 610
 611         update_from_to ();
 612         if (start < from)
 613           {
 614             if (end <= from)
 615               return left.copy (start, end);
 616             left_copy = left.copy (start, from);
 617           }
 618         else if (end > to)
 619           {
 620             if (start >= to)
 621               return right.copy (start, end);
 622             right_copy = right.copy (to, end);
 623           }
 624         this_copy = new MInterval (key, end - start, stack);
 625         this_copy.left = left_copy;
 626         this_copy.right = right_copy;
 627
 628         return this_copy;
 629       }
 630
 631       //  this-.   ==>   this-.
 632       //     right          newright-.
 633       //                            right
 634       private MInterval divide_right (int pos)
 635       {
 636         update_from_to ();
 637
 638         MInterval interval = new MInterval (key, to - pos, stack);
 639
 640         total_length -= to - pos;
 641         to = pos;
 642         if (right != null)
 643           {
 644             right.parent = interval;
 645             interval.total_length += right.total_length;
 646           }
 647         interval.parent = this;
 648         right = interval;
 649         return interval;
 650       }
 651
 652       //    .-this   ==>       .-this
 653       //  left             .-newleft
 654       //                 left
 655       private MInterval divide_left (int pos)
 656       {
 657         update_from_to ();
 658
 659         MInterval interval = new MInterval (key, to - pos, stack);
 660
 661         total_length -= to - pos;
 662         from = pos;
 663         if (left != null)
 664           {
 665             left.parent = interval;
 666             interval.total_length += left.total_length;
 667           }
 668         interval.parent = this;
 669         left = interval;
 670         return interval;
 671       }
 672
 673       private void remove_properties (MTextProperty.Flag flags)
 674       {
 675         for (MPlist p = stack; ! p.IsEmpty;)
 676           {
 677             MTextProperty prop = (MTextProperty) p.Val;
 678
 679             if ((prop.flags & flags) == flags)
 680               p.Pop ();
 681             else
 682               p = p.Next;
 683           }
 684       }
 685
 686       private void merge_properties (MPlist plist, MTextProperty.Flag flags)
 687       {
 688         if (left != null)
 689           left.merge_properties (plist, flags);
 690         if (right != null)
 691           right.merge_properties (plist, flags);
 692         for (MPlist p = plist; ! p.IsEmpty; p = p.Next)
 693           {
 694             MTextProperty prop = (MTextProperty) p.Val;
 695
 696             if ((prop.flags & flags) == flags
 697                 && stack.Get (prop.Key) == null)
 698               stack.Push (prop.key, prop);
 699           }
 700       }
 701
 702       public void insert (int pos, MInterval interval)
 703       {
 704         update_from_to ();
 705         if (pos < from || (pos == from && left == null && pos > 0))
 706           {
 707             prev.insert (pos, interval);
 708             return;
 709           }
 710         if (pos > to || (pos == to && right == null && next != null))
 711           {
 712             next.insert (pos, interval);
 713             return;
 714           }
 715         if (pos > from && pos < to)
 716           {
 717             remove_properties (MTextProperty.Flag.Sensitive);
 718             divide_right (pos).insert (pos, interval);
 719             return;
 720           }
 721         if (pos == from)
 722           {
 723             if (pos > 0)
 724               {
 725                 prev.remove_properties
 726                   (MTextProperty.Flag.Sensitive|MTextProperty.Flag.RearSticky);
 727                 interval.merge_properties
 728                   (prev.stack, MTextProperty.Flag.RearSticky);
 729               }
 730             remove_properties
 731               (MTextProperty.Flag.Sensitive|MTextProperty.Flag.FrontSticky);
 732             interval.merge_properties
 733               (stack, MTextProperty.Flag.FrontSticky);
 734
 735             // INTERVAL is ready to insert.
 736             //
 737             //    .-this-.   ==>          .-this-.
 738             // left-.                  left-.
 739             //     child                  .-interval
 740             //                         child
 741
 742             if (pos > 0)
 743               {
 744                 MInterval i = left.right_most_node;
 745
 746                 i.left = interval;
 747                 interval.parent = i;
 748                 for (; i != null; i = i.parent)
 749                   i.total_length += interval.total_length;
 750               }
 751             else
 752               {
 753                 left = interval;
 754
 755                 for (MInterval i = this; i != null; i = i.parent)
 756                   i.total_length += interval.total_length;
 757               }
 758           }
 759         else                    // pos == to
 760           {
 761             if (right != null)
 762               {
 763                 MInterval left_most = right.left_most_node;
 764
 765                 left_most.remove_properties
 766                   (MTextProperty.Flag.Sensitive|MTextProperty.Flag.FrontSticky);
 767                 interval.merge_properties
 768                   (stack, MTextProperty.Flag.FrontSticky);
 769               }
 770             remove_properties
 771               (MTextProperty.Flag.Sensitive|MTextProperty.Flag.RearSticky);
 772             interval.merge_properties
 773               (stack, MTextProperty.Flag.RearSticky);
 774
 775             // INTERVAL is ready to insert.
 776             //
 777             //    .-this-.   ==>          .-this-.
 778             //         .-right                 .-right
 779             //     child                  interval-.
 780             //                                    child
 781
 782             if (right != null)
 783               {
 784                 MInterval i = right.left_most_node;
 785
 786                 i.left = interval;
 787                 interval.parent = i;
 788                 for (; i != null; i = i.parent)
 789                   i.total_length += interval.total_length;
 790               }
 791             else
 792               {
 793                 right = interval;
 794
 795                 for (MInterval i = this; i != null; i = i.parent)
 796                   i.total_length += interval.total_length;
 797               }
 798           }
 799       }
 800
 801       private void update_parent (MInterval i)
 802       {
 803         if (parent == null)
 804           mtext.intervals.Put (key, i);
 805         else
 806           {
 807             int diff;
 808
 809             if (parent.right == i)
 810               {
 811                 diff = parent.right.total_length - i.total_length;
 812                 parent.right = i;
 813               }
 814             else
 815               {
 816                 diff = parent.left.total_length - i.total_length;
 817                 parent.left = i;
 818               }
 819             for (i = parent; i != null; i = i.parent)
 820               i.total_length += diff;
 821           }
 822       }
 823
 824       public void Delete (int start, int end)
 825       {
 826         update_from_to ();
 827         if (start < from)
 828           {
 829             if (end <= from)
 830               {
 831                 left.Delete (start, end);
 832                 return;
 833               }
 834             left.Delete (start, from);
 835             start = from;
 836           }
 837         else if (end > to)
 838           {
 839             if (start >= to)
 840               {
 841                 right.Delete (start, end);
 842                 return;
 843               }
 844             right.Delete (to, end);
 845             end = to;
 846           }
 847         if (start == from && end == to)
 848           {
 849             if (left == null)
 850               update_parent (right);
 851             else if (right == null)
 852               update_parent (left);
 853             else
 854               {
 855                 MInterval i;
 856
 857                 for (i = right; i.left != null; i = i.left)
 858                   i.total_length += left.total_length;
 859                 i.total_length += left.total_length;
 860                 i.left = left;
 861                 update_parent (right);
 862               }
 863           }
 864         else
 865           {
 866             int len = end - start;
 867
 868             for (MInterval i = this; i != null; i = i.parent)
 869               i.total_length -= len;
 870           }
 871       }
 872
 873       public MTextProperty Push (int start, int end, MTextProperty prop)
 874       {
 875         update_from_to ();
 876         if (start < from)
 877           {
 878             left.Push (start, end, prop);
 879             if (end <= from)
 880               return prop;
 881             start = from;
 882           }
 883         else if (end > to)
 884           {
 885             right.Push (start, end, prop);
 886             if (start >= to)
 887               return prop;
 888             end = to;
 889           }
 890
 891         if (start > from)
 892           divide_left (from);
 893         if (end < to)
 894           divide_right (end);
 895         stack.Push (prop.key, prop);
 896         Console.WriteLine ("push({0},{1})", from, to);
 897         return prop;
 898       }
 899
 900       public Dump ()
 901       {
 902         update_from_to ();
 903
 904         if (left != null)
 905           left.Dump ();
 906         if (stack.IsEmpty)
 907           Console.WriteLine ("({0} {1})", from, to);
 908         else
 909           Console.WriteLine ("({0} {1} {2})", from, to, stack.Val);
 910         if (right != null)
 911           right.Dump ();
 912       }
 913     }
 914
 915     private class MTextEnum : IEnumerator
 916     {
 917       private MText mt;
 918       private int pos = -1;
 919
 920       public MTextEnum (MText mt)
 921         {
 922           this.mt = mt;
 923         }
 924
 925       public bool MoveNext ()
 926       {
 927         pos++;
 928         return (pos < mt.nchars);
 929       }
 930
 931       public void Reset ()
 932       {
 933         pos = -1;
 934       }
 935
 936       public object Current
 937       {
 938         get {
 939           //if (pos < 0 || pos >= mt.nchars)
 940           //throw new InvalidOperationException ();
 941           return mt[pos];
 942         }
 943       }
 944     }
 945   }
 946 }