--- 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],
--- 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] =