src/Tools/jEdit/src/proofdocument/Text.scala
changeset 34654 30f588245884
parent 34652 5fe5e00ec430
--- a/src/Tools/jEdit/src/proofdocument/Text.scala	Wed Jul 08 15:15:15 2009 +0200
+++ b/src/Tools/jEdit/src/proofdocument/Text.scala	Mon Jul 13 14:30:39 2009 +0200
@@ -9,11 +9,15 @@
 
 object Text {
   case class Change(
-    base_id: String,
+    base: Option[Change],
     id: String,
     start: Int,
     added: String,
-    removed: String) {
+    removed: String)
+  {
     override def toString = id + ": added '" + added + "'; removed '" + removed + "'"
+
+    def ancestors: List[Text.Change] =
+      this :: base.map(_.ancestors).getOrElse(Nil)
   }
-}
\ No newline at end of file
+}