author | wenzelm |
Thu, 05 Aug 2010 14:35:35 +0200 | |
changeset 38150 | 67fc24df3721 |
parent 36676 | ac7961d42ac3 |
child 38151 | 2837c952ca31 |
permissions | -rw-r--r-- |
36676 | 1 |
/* Title: Pure/PIDE/change.scala |
2 |
Author: Fabian Immler, TU Munich |
|
3 |
Author: Makarius |
|
4 |
||
5 |
Changes of plain text. |
|
6 |
*/ |
|
34660 | 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 |
|
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
36676
diff
changeset
|
11 |
object Change |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
36676
diff
changeset
|
12 |
{ |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
36676
diff
changeset
|
13 |
val init = new Change(Document.NO_ID, None, Nil, Future.value(Nil, Document.init)) |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
36676
diff
changeset
|
14 |
} |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
36676
diff
changeset
|
15 |
|
34660 | 16 |
class Change( |
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
36676
diff
changeset
|
17 |
val id: Document.Version_ID, |
34660 | 18 |
val parent: Option[Change], |
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
36676
diff
changeset
|
19 |
val edits: List[Document.Node.Text_Edit], |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
36676
diff
changeset
|
20 |
val result: Future[(List[Document.Edit[Command]], Document)]) |
34660 | 21 |
{ |
34833
683ddf358698
recovered explicit Changed.id (copy of future document) -- avoids premature joining of result;
wenzelm
parents:
34827
diff
changeset
|
22 |
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
|
23 |
{ |
683ddf358698
recovered explicit Changed.id (copy of future document) -- avoids premature joining of result;
wenzelm
parents:
34827
diff
changeset
|
24 |
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
|
25 |
def hasNext = state.isDefined |
683ddf358698
recovered explicit Changed.id (copy of future document) -- avoids premature joining of result;
wenzelm
parents:
34827
diff
changeset
|
26 |
def next = |
683ddf358698
recovered explicit Changed.id (copy of future document) -- avoids premature joining of result;
wenzelm
parents:
34827
diff
changeset
|
27 |
state match { |
683ddf358698
recovered explicit Changed.id (copy of future document) -- avoids premature joining of result;
wenzelm
parents:
34827
diff
changeset
|
28 |
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
|
29 |
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
|
30 |
} |
683ddf358698
recovered explicit Changed.id (copy of future document) -- avoids premature joining of result;
wenzelm
parents:
34827
diff
changeset
|
31 |
} |
34660 | 32 |
|
34853
32b49207ca20
misc tuning and clarification of Document/Change;
wenzelm
parents:
34838
diff
changeset
|
33 |
def join_document: Document = result.join._2 |
34854 | 34 |
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
|
35 |
|
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
36676
diff
changeset
|
36 |
def edit(session: Session, edits: List[Document.Node.Text_Edit]): Change = |
34853
32b49207ca20
misc tuning and clarification of Document/Change;
wenzelm
parents:
34838
diff
changeset
|
37 |
{ |
32b49207ca20
misc tuning and clarification of Document/Change;
wenzelm
parents:
34838
diff
changeset
|
38 |
val new_id = session.create_id() |
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
36676
diff
changeset
|
39 |
val result: Future[(List[Document.Edit[Command]], Document)] = |
34853
32b49207ca20
misc tuning and clarification of Document/Change;
wenzelm
parents:
34838
diff
changeset
|
40 |
Future.fork { |
32b49207ca20
misc tuning and clarification of Document/Change;
wenzelm
parents:
34838
diff
changeset
|
41 |
val old_doc = join_document |
32b49207ca20
misc tuning and clarification of Document/Change;
wenzelm
parents:
34838
diff
changeset
|
42 |
old_doc.await_assignment |
32b49207ca20
misc tuning and clarification of Document/Change;
wenzelm
parents:
34838
diff
changeset
|
43 |
Document.text_edits(session, old_doc, new_id, edits) |
32b49207ca20
misc tuning and clarification of Document/Change;
wenzelm
parents:
34838
diff
changeset
|
44 |
} |
32b49207ca20
misc tuning and clarification of Document/Change;
wenzelm
parents:
34838
diff
changeset
|
45 |
new Change(new_id, Some(this), edits, result) |
32b49207ca20
misc tuning and clarification of Document/Change;
wenzelm
parents:
34838
diff
changeset
|
46 |
} |
34660 | 47 |
} |