tuned signature;
authorwenzelm
Thu Aug 25 13:24:41 2011 +0200 (2011-08-25 ago)
changeset 44475709e1d671483
parent 44474 681447a9ffe5
child 44476 e8a87398f35d
tuned signature;
src/Pure/PIDE/document.scala
src/Pure/System/session.scala
     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],
     2.1 --- a/src/Pure/System/session.scala	Thu Aug 25 11:41:48 2011 +0200
     2.2 +++ b/src/Pure/System/session.scala	Thu Aug 25 13:24:41 2011 +0200
     2.3 @@ -206,7 +206,7 @@
     2.4  
     2.5      def update_perspective(name: String, text_perspective: Text.Perspective)
     2.6      {
     2.7 -      val previous = global_state().history.tip.version.get_finished
     2.8 +      val previous = global_state().tip_version
     2.9        val (perspective, version) = Thy_Syntax.edit_perspective(previous, name, text_perspective)
    2.10  
    2.11        val text_edits: List[Document.Edit_Text] =