author | wenzelm |
Mon, 11 Jan 2010 23:00:05 +0100 | |
changeset 34871 | e596a0b71f3c |
parent 34854 | src/Tools/jEdit/src/proofdocument/change.scala@64c2eb92df9f |
permissions | -rw-r--r-- |
34660 | 1 |
/* |
34703 | 2 |
* Changes of plain text |
34660 | 3 |
* |
4 |
* @author Fabian Immler, TU Munich |
|
34838 | 5 |
* @author Makarius |
34660 | 6 |
*/ |
7 |
||
34871
e596a0b71f3c
incorporate "proofdocument" part into main Isabelle/Pure.jar -- except for html_panel.scala, which depends on external library (Lobo/Cobra browser);
wenzelm
parents:
34854
diff
changeset
|
8 |
package isabelle |
34660 | 9 |
|
34703 | 10 |
|
34660 | 11 |
class Change( |
34853
32b49207ca20
misc tuning and clarification of Document/Change;
wenzelm
parents:
34838
diff
changeset
|
12 |
val id: Isar_Document.Document_ID, |
34660 | 13 |
val parent: Option[Change], |
34838 | 14 |
val edits: List[Text_Edit], |
34853
32b49207ca20
misc tuning and clarification of Document/Change;
wenzelm
parents:
34838
diff
changeset
|
15 |
val result: Future[(List[Document.Edit], Document)]) |
34660 | 16 |
{ |
34833
683ddf358698
recovered explicit Changed.id (copy of future document) -- avoids premature joining of result;
wenzelm
parents:
34827
diff
changeset
|
17 |
def ancestors: Iterator[Change] = new Iterator[Change] |
683ddf358698
recovered explicit Changed.id (copy of future document) -- avoids premature joining of result;
wenzelm
parents:
34827
diff
changeset
|
18 |
{ |
683ddf358698
recovered explicit Changed.id (copy of future document) -- avoids premature joining of result;
wenzelm
parents:
34827
diff
changeset
|
19 |
private var state: Option[Change] = Some(Change.this) |
683ddf358698
recovered explicit Changed.id (copy of future document) -- avoids premature joining of result;
wenzelm
parents:
34827
diff
changeset
|
20 |
def hasNext = state.isDefined |
683ddf358698
recovered explicit Changed.id (copy of future document) -- avoids premature joining of result;
wenzelm
parents:
34827
diff
changeset
|
21 |
def next = |
683ddf358698
recovered explicit Changed.id (copy of future document) -- avoids premature joining of result;
wenzelm
parents:
34827
diff
changeset
|
22 |
state match { |
683ddf358698
recovered explicit Changed.id (copy of future document) -- avoids premature joining of result;
wenzelm
parents:
34827
diff
changeset
|
23 |
case Some(change) => state = change.parent; change |
683ddf358698
recovered explicit Changed.id (copy of future document) -- avoids premature joining of result;
wenzelm
parents:
34827
diff
changeset
|
24 |
case None => throw new NoSuchElementException("next on empty iterator") |
683ddf358698
recovered explicit Changed.id (copy of future document) -- avoids premature joining of result;
wenzelm
parents:
34827
diff
changeset
|
25 |
} |
683ddf358698
recovered explicit Changed.id (copy of future document) -- avoids premature joining of result;
wenzelm
parents:
34827
diff
changeset
|
26 |
} |
34660 | 27 |
|
34853
32b49207ca20
misc tuning and clarification of Document/Change;
wenzelm
parents:
34838
diff
changeset
|
28 |
def join_document: Document = result.join._2 |
34854 | 29 |
def is_assigned: Boolean = result.is_finished && join_document.assignment.is_finished |
34853
32b49207ca20
misc tuning and clarification of Document/Change;
wenzelm
parents:
34838
diff
changeset
|
30 |
|
32b49207ca20
misc tuning and clarification of Document/Change;
wenzelm
parents:
34838
diff
changeset
|
31 |
def edit(session: Session, edits: List[Text_Edit]): Change = |
32b49207ca20
misc tuning and clarification of Document/Change;
wenzelm
parents:
34838
diff
changeset
|
32 |
{ |
32b49207ca20
misc tuning and clarification of Document/Change;
wenzelm
parents:
34838
diff
changeset
|
33 |
val new_id = session.create_id() |
32b49207ca20
misc tuning and clarification of Document/Change;
wenzelm
parents:
34838
diff
changeset
|
34 |
val result: Future[(List[Document.Edit], Document)] = |
32b49207ca20
misc tuning and clarification of Document/Change;
wenzelm
parents:
34838
diff
changeset
|
35 |
Future.fork { |
32b49207ca20
misc tuning and clarification of Document/Change;
wenzelm
parents:
34838
diff
changeset
|
36 |
val old_doc = join_document |
32b49207ca20
misc tuning and clarification of Document/Change;
wenzelm
parents:
34838
diff
changeset
|
37 |
old_doc.await_assignment |
32b49207ca20
misc tuning and clarification of Document/Change;
wenzelm
parents:
34838
diff
changeset
|
38 |
Document.text_edits(session, old_doc, new_id, edits) |
32b49207ca20
misc tuning and clarification of Document/Change;
wenzelm
parents:
34838
diff
changeset
|
39 |
} |
32b49207ca20
misc tuning and clarification of Document/Change;
wenzelm
parents:
34838
diff
changeset
|
40 |
new Change(new_id, Some(this), edits, result) |
32b49207ca20
misc tuning and clarification of Document/Change;
wenzelm
parents:
34838
diff
changeset
|
41 |
} |
34660 | 42 |
} |