--- a/src/Pure/PIDE/document.scala Fri Sep 24 21:05:07 2010 +0200
+++ b/src/Pure/PIDE/document.scala Sat Sep 25 13:57:34 2010 +0200
@@ -136,8 +136,8 @@
val edits: List[Node_Text_Edit],
val result: Future[(List[Edit[Command]], Version)])
{
- val current: Future[Version] = result.map(_._2)
- def is_finished: Boolean = previous.is_finished && current.is_finished
+ val version: Future[Version] = result.map(_._2)
+ def is_finished: Boolean = previous.is_finished && version.is_finished
}
@@ -279,7 +279,7 @@
def snapshot(name: String, pending_edits: List[Text.Edit]): Snapshot =
{
val found_stable = history.undo_list.find(change =>
- change.is_finished && is_assigned(change.current.get_finished))
+ change.is_finished && is_assigned(change.version.get_finished))
require(found_stable.isDefined)
val stable = found_stable.get
val latest = history.undo_list.head
@@ -291,7 +291,7 @@
new Snapshot
{
- val version = stable.current.get_finished
+ val version = stable.version.get_finished
val node = version.nodes(name)
val is_outdated = !(pending_edits.isEmpty && latest == stable)