# HG changeset patch
# User wenzelm
# Date 1262712219 -3600
# Node ID 08a72dc4868e1106ee2e6a1bb2ba7c2a492d45f2
# Parent  aa73039d5d148df38229252ae10918f98ea29dd6
use Text_Edit provided by Isabelle;

diff -r aa73039d5d14 -r 08a72dc4868e src/Tools/jEdit/src/jedit/document_model.scala
--- a/src/Tools/jEdit/src/jedit/document_model.scala	Tue Jan 05 18:23:15 2010 +0100
+++ b/src/Tools/jEdit/src/jedit/document_model.scala	Tue Jan 05 18:23:39 2010 +0100
@@ -8,7 +8,7 @@
 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
@@ -77,7 +77,7 @@
 
   /* 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 /:
@@ -99,7 +99,7 @@
 
   /* 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) {
@@ -124,14 +124,14 @@
     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()
     }
   }
@@ -145,7 +145,7 @@
     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()
   }
 
diff -r aa73039d5d14 -r 08a72dc4868e src/Tools/jEdit/src/proofdocument/change.scala
--- a/src/Tools/jEdit/src/proofdocument/change.scala	Tue Jan 05 18:23:15 2010 +0100
+++ b/src/Tools/jEdit/src/proofdocument/change.scala	Tue Jan 05 18:23:39 2010 +0100
@@ -1,47 +1,16 @@
 /*
  * Changes of plain text
  *
- * @author Johannes Hölzl, TU Munich
  * @author Fabian Immler, TU Munich
+ * @author Makarius
  */
 
 package isabelle.proofdocument
 
 
-sealed abstract class Edit
-{
-  val start: Int
-  def before(offset: Int): Int
-  def after(offset: Int): Int
-}
-
-
-case class Insert(start: Int, text: String) extends Edit
-{
-  def before(offset: Int): Int =
-    if (start > offset) offset
-    else (offset - text.length) max start
-
-  def after(offset: Int): Int =
-    if (start <= offset) offset + text.length else offset
-}
-
-
-case class Remove(start: Int, text: String) extends Edit
-{
-  def before(offset: Int): Int =
-    if (start <= offset) offset + text.length else offset
-
-  def after(offset: Int): Int =
-    if (start > offset) offset
-    else (offset - text.length) max start
-}
-// TODO: merge multiple inserts?
-
-
 class Change(
   val parent: Option[Change],
-  val edits: List[Edit],
+  val edits: List[Text_Edit],
   val id: Isar_Document.Document_ID,
   val result: Future[Document.Result])
 {
diff -r aa73039d5d14 -r 08a72dc4868e src/Tools/jEdit/src/proofdocument/document.scala
--- a/src/Tools/jEdit/src/proofdocument/document.scala	Tue Jan 05 18:23:15 2010 +0100
+++ b/src/Tools/jEdit/src/proofdocument/document.scala	Tue Jan 05 18:23:39 2010 +0100
@@ -45,10 +45,10 @@
   type Result = (Document, List[Structure_Edit])
 
   def text_edits(session: Session, old_doc: Document, new_id: Isar_Document.Document_ID,
-    edits: List[Edit]): Result =
+    edits: List[Text_Edit]): Result =
   {
     val changes = new mutable.ListBuffer[Structure_Edit]
-    val new_doc = (old_doc /: edits)((doc1: Document, edit: Edit) =>
+    val new_doc = (old_doc /: edits)((doc1: Document, edit: Text_Edit) =>
       {
         val (doc2, chgs) = doc1.text_edit(session, edit, new_id)  // FIXME odd multiple use of id
         changes ++ chgs
@@ -92,12 +92,12 @@
 
   /** token view **/
 
-  def text_edit(session: Session, e: Edit, id: String): Document.Result =
+  def text_edit(session: Session, e: Text_Edit, id: String): Document.Result =
   {
     case class TextChange(start: Int, added: String, removed: String)
     val change = e match {
-      case Insert(s, a) => TextChange(s, a, "")
-      case Remove(s, r) => TextChange(s, "", r)
+      case Text_Edit.Insert(s, a) => TextChange(s, a, "")
+      case Text_Edit.Remove(s, r) => TextChange(s, "", r)
     }
     //indices of tokens
     var start: Map[Token, Int] = token_start