# HG changeset patch
# User wenzelm
# Date 1439657971 -7200
# Node ID 6d03e05ef041351b31cf33fd02219c977b0c4673
# Parent  13ee73f57c853f5412a3cda72d6f3a853be46d3f
more robust access to stable tip version: take all pending edits into account, don't assume model for current buffer;

diff -r 13ee73f57c85 -r 6d03e05ef041 src/Pure/PIDE/document.scala
--- 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],
diff -r 13ee73f57c85 -r 6d03e05ef041 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())
 
diff -r 13ee73f57c85 -r 6d03e05ef041 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 */
 
diff -r 13ee73f57c85 -r 6d03e05ef041 src/Tools/jEdit/src/plugin.scala
--- 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