equal
deleted
inserted
replaced
1 /* |
|
2 * Changes of plain text |
|
3 * |
|
4 * @author Fabian Immler, TU Munich |
|
5 * @author Makarius |
|
6 */ |
|
7 |
|
8 package isabelle.proofdocument |
|
9 |
|
10 |
|
11 class Change( |
|
12 val id: Isar_Document.Document_ID, |
|
13 val parent: Option[Change], |
|
14 val edits: List[Text_Edit], |
|
15 val result: Future[(List[Document.Edit], Document)]) |
|
16 { |
|
17 def ancestors: Iterator[Change] = new Iterator[Change] |
|
18 { |
|
19 private var state: Option[Change] = Some(Change.this) |
|
20 def hasNext = state.isDefined |
|
21 def next = |
|
22 state match { |
|
23 case Some(change) => state = change.parent; change |
|
24 case None => throw new NoSuchElementException("next on empty iterator") |
|
25 } |
|
26 } |
|
27 |
|
28 def join_document: Document = result.join._2 |
|
29 def is_assigned: Boolean = result.is_finished && join_document.assignment.is_finished |
|
30 |
|
31 def edit(session: Session, edits: List[Text_Edit]): Change = |
|
32 { |
|
33 val new_id = session.create_id() |
|
34 val result: Future[(List[Document.Edit], Document)] = |
|
35 Future.fork { |
|
36 val old_doc = join_document |
|
37 old_doc.await_assignment |
|
38 Document.text_edits(session, old_doc, new_id, edits) |
|
39 } |
|
40 new Change(new_id, Some(this), edits, result) |
|
41 } |
|
42 } |
|