1.1 --- a/src/Tools/jEdit/src/jedit/document_model.scala	Mon Jan 11 16:49:11 2010 +0100
     1.2 +++ b/src/Tools/jEdit/src/jedit/document_model.scala	Mon Jan 11 18:26:13 2010 +0100
     1.3 @@ -112,14 +112,14 @@
     1.4      override def contentInserted(buffer: JEditBuffer,
     1.5        start_line: Int, offset: Int, num_lines: Int, length: Int)
     1.6      {
     1.7 -      edits_buffer += Text_Edit.Insert(offset, buffer.getText(offset, length))
     1.8 +      edits_buffer += new Text_Edit(true, offset, buffer.getText(offset, length))
     1.9        edits_delay()
    1.10      }
    1.11  
    1.12      override def preContentRemoved(buffer: JEditBuffer,
    1.13        start_line: Int, start: Int, num_lines: Int, removed_length: Int)
    1.14      {
    1.15 -      edits_buffer += Text_Edit.Remove(start, buffer.getText(start, removed_length))
    1.16 +      edits_buffer += new Text_Edit(false, start, buffer.getText(start, removed_length))
    1.17        edits_delay()
    1.18      }
    1.19    }
    1.20 @@ -133,7 +133,7 @@
    1.21      buffer.addBufferListener(buffer_listener)
    1.22      buffer.propertiesChanged()
    1.23  
    1.24 -    edits_buffer += Text_Edit.Insert(0, buffer.getText(0, buffer.getLength))
    1.25 +    edits_buffer += new Text_Edit(true, 0, buffer.getText(0, buffer.getLength))
    1.26      edits_delay()
    1.27    }
    1.28