src/Tools/jEdit/src/document_model.scala

--- a/src/Tools/jEdit/src/document_model.scala	Sat Aug 15 17:38:20 2015 +0200
+++ b/src/Tools/jEdit/src/document_model.scala	Sat Aug 15 18:59:31 2015 +0200
@@ -264,6 +264,8 @@
     }
   }
 
+  def is_stable(): Boolean = !pending_edits.is_pending();
+
   def snapshot(): Document.Snapshot =
     session.snapshot(node_name, pending_edits.snapshot())