src/Tools/jEdit/src/proofdocument/change.scala

tuned Change: eliminated redundant copy of document id;

/*
 * 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 parent: Option[Change],
  val edits: List[Edit],
  val result: Future[Document.Result])
{
  // FIXME iterator
  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)

  def document: Document = result.join._1
  def document_edits: List[Document.Structure_Edit] = result.join._2
}