# HG changeset patch
# User wenzelm
# Date 1314271481 -7200
# Node ID 709e1d67148358301e03684acb4f4c616ffcc18b
# Parent  681447a9ffe58ed3fff7dada691ea42476d87b5f
tuned signature;

diff -r 681447a9ffe5 -r 709e1d671483 src/Pure/PIDE/document.scala
--- 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],
diff -r 681447a9ffe5 -r 709e1d671483 src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Thu Aug 25 11:41:48 2011 +0200
+++ b/src/Pure/System/session.scala	Thu Aug 25 13:24:41 2011 +0200
@@ -206,7 +206,7 @@
 
     def update_perspective(name: String, text_perspective: Text.Perspective)
     {
-      val previous = global_state().history.tip.version.get_finished
+      val previous = global_state().tip_version
       val (perspective, version) = Thy_Syntax.edit_perspective(previous, name, text_perspective)
 
       val text_edits: List[Document.Edit_Text] =