src/Tools/jEdit/src/proofdocument/Change.scala

--- a/src/Tools/jEdit/src/proofdocument/Change.scala	Tue Sep 01 21:05:57 2009 +0200
+++ b/src/Tools/jEdit/src/proofdocument/Change.scala	Wed Sep 02 21:21:54 2009 +0200
@@ -7,41 +7,42 @@
 
 package isabelle.proofdocument
 
-abstract class Edit {
+sealed abstract class Edit
+{
   val start: Int
   def from_where (x: Int): Int //where has x been before applying this edit
   def where_to(x: Int): Int //where will x be when we apply this edit
 }
 
-case class Insert(start: Int, added: String) extends Edit {
+case class Insert(start: Int, text: String) extends Edit
+{
   def from_where(x: Int) =
     if (start > x) x
-    else (x - added.length) max start
+    else (x - text.length) max start
 
   def where_to(x: Int) =
-    if (start <= x) x + added.length else x
+    if (start <= x) x + text.length else x
 }
 
-case class Remove(start: Int, removed: String) extends Edit {
+case class Remove(start: Int, text: String) extends Edit
+{
   def from_where(x: Int) =
-    if (start <= x) x + removed.length else x
+    if (start <= x) x + text.length else x
 
   def where_to(x: Int) =
     if (start > x) x
-    else (x - removed.length) max start
+    else (x - text.length) max start
 }
 // TODO: merge multiple inserts?
 
 class Change(
   val id: String,
   val parent: Option[Change],
-  edits: List[Edit]) extends Iterable[Edit]
+  val edits: List[Edit])
 {
-  override def elements = edits.reverse.elements
-
-  def ancestors(root_p: Change => Boolean): List[Change] =
-    if (root_p(this)) Nil
-    else this :: parent.map(_.ancestors(root_p)).getOrElse(Nil)
+  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 =