--- a/src/Pure/PIDE/document.scala Thu Aug 25 11:41:48 2011 +0200
+++ b/src/Pure/PIDE/document.scala Thu Aug 25 13:24:41 2011 +0200
@@ -296,8 +296,9 @@
def is_stable(change: Change): Boolean =
change.is_finished && is_assigned(change.version.get_finished)
+ def recent_stable: Option[Change] = history.undo_list.find(is_stable)
def tip_stable: Boolean = is_stable(history.tip)
- def recent_stable: Option[Change] = history.undo_list.find(is_stable)
+ def tip_version: Version = history.tip.version.get_finished
def continue_history(
previous: Future[Version],