changeset 60933 | 6d03e05ef041 |
parent 60274 | c2837a39da01 |
child 61192 | 98eba31c51f8 |
--- 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())