1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/Thy/change.scala	Mon Jan 11 23:00:05 2010 +0100
     1.3 @@ -0,0 +1,42 @@
     1.4 +/*
     1.5 + * Changes of plain text
     1.6 + *
     1.7 + * @author Fabian Immler, TU Munich
     1.8 + * @author Makarius
     1.9 + */
    1.10 +
    1.11 +package isabelle
    1.12 +
    1.13 +
    1.14 +class Change(
    1.15 +  val id: Isar_Document.Document_ID,
    1.16 +  val parent: Option[Change],
    1.17 +  val edits: List[Text_Edit],
    1.18 +  val result: Future[(List[Document.Edit], Document)])
    1.19 +{
    1.20 +  def ancestors: Iterator[Change] = new Iterator[Change]
    1.21 +  {
    1.22 +    private var state: Option[Change] = Some(Change.this)
    1.23 +    def hasNext = state.isDefined
    1.24 +    def next =
    1.25 +      state match {
    1.26 +        case Some(change) => state = change.parent; change
    1.27 +        case None => throw new NoSuchElementException("next on empty iterator")
    1.28 +      }
    1.29 +  }
    1.30 +
    1.31 +  def join_document: Document = result.join._2
    1.32 +  def is_assigned: Boolean = result.is_finished && join_document.assignment.is_finished
    1.33 +
    1.34 +  def edit(session: Session, edits: List[Text_Edit]): Change =
    1.35 +  {
    1.36 +    val new_id = session.create_id()
    1.37 +    val result: Future[(List[Document.Edit], Document)] =
    1.38 +      Future.fork {
    1.39 +        val old_doc = join_document
    1.40 +        old_doc.await_assignment
    1.41 +        Document.text_edits(session, old_doc, new_id, edits)
    1.42 +      }
    1.43 +    new Change(new_id, Some(this), edits, result)
    1.44 +  }
    1.45 +}
    1.46 \ No newline at end of file