--- 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
+}