src/Pure/PIDE/document.scala
changeset 44475 709e1d671483
parent 44474 681447a9ffe5
child 44476 e8a87398f35d
     1.1 --- a/src/Pure/PIDE/document.scala	Thu Aug 25 11:41:48 2011 +0200
     1.2 +++ b/src/Pure/PIDE/document.scala	Thu Aug 25 13:24:41 2011 +0200
     1.3 @@ -296,8 +296,9 @@
     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_stable: Option[Change] = history.undo_list.find(is_stable)
     1.8      def tip_stable: Boolean = is_stable(history.tip)
     1.9 -    def recent_stable: Option[Change] = history.undo_list.find(is_stable)
    1.10 +    def tip_version: Version = history.tip.version.get_finished
    1.11  
    1.12      def continue_history(
    1.13          previous: Future[Version],