more robust access to stable tip version: take all pending edits into account, don't assume model for current buffer;
--- a/src/Pure/PIDE/document.scala Sat Aug 15 17:38:20 2015 +0200
+++ b/src/Pure/PIDE/document.scala Sat Aug 15 18:59:31 2015 +0200
@@ -632,8 +632,8 @@
def recent_finished: Change = history.undo_list.find(_.is_finished) getOrElse fail
def recent_stable: Change = history.undo_list.find(is_stable) getOrElse fail
- def tip_stable: Boolean = is_stable(history.tip)
- def tip_version: Version = history.tip.version.get_finished
+ def stable_tip_version: Option[Version] =
+ if (is_stable(history.tip)) Some(history.tip.version.get_finished) else None
def continue_history(
previous: Future[Version],
--- 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())
--- 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 */
--- a/src/Tools/jEdit/src/plugin.scala Sat Aug 15 17:38:20 2015 +0200
+++ b/src/Tools/jEdit/src/plugin.scala Sat Aug 15 18:59:31 2015 +0200
@@ -221,9 +221,10 @@
val aux_files =
if (PIDE.options.bool("jedit_auto_resolve")) {
- val snapshot = PIDE.snapshot(view)
- if (snapshot.is_outdated) Nil
- else snapshot.version.nodes.undefined_blobs.map(_.node)
+ PIDE.editor.stable_tip_version() match {
+ case Some(version) => version.nodes.undefined_blobs.map(_.node)
+ case None => Nil
+ }
}
else Nil