src/Tools/jEdit/src/jedit_editor.scala

--- a/src/Tools/jEdit/src/jedit_editor.scala	Sat Aug 15 17:38:20 2015 +0200
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Sat Aug 15 18:59:31 2015 +0200
@@ -49,6 +49,13 @@
 
   def invoke(): Unit = delay_flush.invoke()
 
+  def stable_tip_version(): Option[Document.Version] =
+    GUI_Thread.require {
+      if (removed_nodes.isEmpty && PIDE.document_models().forall(_.is_stable))
+        session.current_state().stable_tip_version
+      else None
+    }
+
 
   /* current situation */