--- a/src/Tools/jEdit/src/proofdocument/change.scala Sun Jan 10 15:42:31 2010 +0100
+++ b/src/Tools/jEdit/src/proofdocument/change.scala Sun Jan 10 16:40:21 2010 +0100
@@ -9,10 +9,10 @@
class Change(
+ val id: Isar_Document.Document_ID,
val parent: Option[Change],
val edits: List[Text_Edit],
- val id: Isar_Document.Document_ID,
- val result: Future[Document.Result])
+ val result: Future[(List[Document.Edit], Document)])
{
def ancestors: Iterator[Change] = new Iterator[Change]
{
@@ -25,6 +25,17 @@
}
}
- def document: Document = result.join._1
- def document_edits: List[Document.Structure_Edit] = result.join._2
+ def join_document: Document = result.join._2
+
+ def edit(session: Session, edits: List[Text_Edit]): Change =
+ {
+ val new_id = session.create_id()
+ val result: Future[(List[Document.Edit], Document)] =
+ Future.fork {
+ val old_doc = join_document
+ old_doc.await_assignment
+ Document.text_edits(session, old_doc, new_id, edits)
+ }
+ new Change(new_id, Some(this), edits, result)
+ }
}
\ No newline at end of file