src/Pure/PIDE/document.scala
changeset 46944 9fc22eb6408c
parent 46942 f5c2d66faa04
child 46997 395b7277ed76
     1.1 --- a/src/Pure/PIDE/document.scala	Thu Mar 15 14:22:54 2012 +0100
     1.2 +++ b/src/Pure/PIDE/document.scala	Thu Mar 15 14:39:42 2012 +0100
     1.3 @@ -419,6 +419,7 @@
     1.4      def is_stable(change: Change): Boolean =
     1.5        change.is_finished && is_assigned(change.version.get_finished)
     1.6  
     1.7 +    def recent_finished: Change = history.undo_list.find(_.is_finished) getOrElse fail
     1.8      def recent_stable: Change = history.undo_list.find(is_stable) getOrElse fail
     1.9      def tip_stable: Boolean = is_stable(history.tip)
    1.10      def tip_version: Version = history.tip.version.get_finished