src/Tools/jEdit/src/jedit/document_model.scala

  */
 
 package isabelle.jedit
 
 
-import isabelle.proofdocument.{Change, Command, Edit, Insert, Remove, Document, Session}
+import isabelle.proofdocument.{Change, Command, Document, Session}
 
 import scala.actors.Actor, Actor._
 import scala.collection.mutable
 
 import org.gjt.sp.jedit.Buffer

   }
 
 
   /* transforming offsets */
 
-  private def changes_from(doc: Document): List[Edit] =
+  private def changes_from(doc: Document): List[Text_Edit] =
   {
     Swing_Thread.assert()
     (edits_buffer.toList /:
       current_change.ancestors.takeWhile(_.id != doc.id))((edits, change) => change.edits ::: edits)
   }

   }
 
 
   /* text edits */
 
-  private val edits_buffer = new mutable.ListBuffer[Edit]   // owned by Swing thread
+  private val edits_buffer = new mutable.ListBuffer[Text_Edit]   // owned by Swing thread
 
   private val edits_delay = Swing_Thread.delay_last(300) {
     if (!edits_buffer.isEmpty) {
       val edits = edits_buffer.toList
       val change1 = current_change()

   private val buffer_listener: BufferListener = new BufferAdapter
   {
     override def contentInserted(buffer: JEditBuffer,
       start_line: Int, offset: Int, num_lines: Int, length: Int)
     {
-      edits_buffer += Insert(offset, buffer.getText(offset, length))
+      edits_buffer += Text_Edit.Insert(offset, buffer.getText(offset, length))
       edits_delay()
     }
 
     override def preContentRemoved(buffer: JEditBuffer,
       start_line: Int, start: Int, num_lines: Int, removed_length: Int)
     {
-      edits_buffer += Remove(start, buffer.getText(start, removed_length))
+      edits_buffer += Text_Edit.Remove(start, buffer.getText(start, removed_length))
       edits_delay()
     }
   }
 
 

   {
     buffer.setTokenMarker(new Isabelle_Token_Marker(this))
     buffer.addBufferListener(buffer_listener)
     buffer.propertiesChanged()
 
-    edits_buffer += Insert(0, buffer.getText(0, buffer.getLength))
+    edits_buffer += Text_Edit.Insert(0, buffer.getText(0, buffer.getLength))
     edits_delay()
   }
 
   def deactivate()
   {