--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/proofdocument/change.scala Tue Dec 08 14:49:01 2009 +0100
@@ -0,0 +1,54 @@
+/*
+ * Changes of plain text
+ *
+ * @author Johannes Hölzl, TU Munich
+ * @author Fabian Immler, TU Munich
+ */
+
+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 id: String,
+ val parent: Option[Change],
+ val edits: List[Edit])
+{
+ def ancestors(done: Change => Boolean): List[Change] =
+ if (done(this)) Nil
+ else this :: parent.map(_.ancestors(done)).getOrElse(Nil)
+ def ancestors: List[Change] = ancestors(_ => false)
+
+ override def toString =
+ "Change(" + id + " <- " + parent.map(_.id) + ", " + edits + ")"
+}
\ No newline at end of file