more robust access to stable tip version: take all pending edits into account, don't assume model for current buffer;
authorwenzelm
Sat Aug 15 18:59:31 2015 +0200 (2015-08-15)
changeset 609336d03e05ef041
parent 60932 13ee73f57c85
child 60934 b63d0ff4b797
more robust access to stable tip version: take all pending edits into account, don't assume model for current buffer;
src/Pure/PIDE/document.scala
src/Tools/jEdit/src/document_model.scala
src/Tools/jEdit/src/jedit_editor.scala
src/Tools/jEdit/src/plugin.scala
     1.1 --- a/src/Pure/PIDE/document.scala	Sat Aug 15 17:38:20 2015 +0200
     1.2 +++ b/src/Pure/PIDE/document.scala	Sat Aug 15 18:59:31 2015 +0200
     1.3 @@ -632,8 +632,8 @@
     1.4  
     1.5      def recent_finished: Change = history.undo_list.find(_.is_finished) getOrElse fail
     1.6      def recent_stable: Change = history.undo_list.find(is_stable) getOrElse fail
     1.7 -    def tip_stable: Boolean = is_stable(history.tip)
     1.8 -    def tip_version: Version = history.tip.version.get_finished
     1.9 +    def stable_tip_version: Option[Version] =
    1.10 +      if (is_stable(history.tip)) Some(history.tip.version.get_finished) else None
    1.11  
    1.12      def continue_history(
    1.13        previous: Future[Version],
     2.1 --- a/src/Tools/jEdit/src/document_model.scala	Sat Aug 15 17:38:20 2015 +0200
     2.2 +++ b/src/Tools/jEdit/src/document_model.scala	Sat Aug 15 18:59:31 2015 +0200
     2.3 @@ -264,6 +264,8 @@
     2.4      }
     2.5    }
     2.6  
     2.7 +  def is_stable(): Boolean = !pending_edits.is_pending();
     2.8 +
     2.9    def snapshot(): Document.Snapshot =
    2.10      session.snapshot(node_name, pending_edits.snapshot())
    2.11  
     3.1 --- a/src/Tools/jEdit/src/jedit_editor.scala	Sat Aug 15 17:38:20 2015 +0200
     3.2 +++ b/src/Tools/jEdit/src/jedit_editor.scala	Sat Aug 15 18:59:31 2015 +0200
     3.3 @@ -49,6 +49,13 @@
     3.4  
     3.5    def invoke(): Unit = delay_flush.invoke()
     3.6  
     3.7 +  def stable_tip_version(): Option[Document.Version] =
     3.8 +    GUI_Thread.require {
     3.9 +      if (removed_nodes.isEmpty && PIDE.document_models().forall(_.is_stable))
    3.10 +        session.current_state().stable_tip_version
    3.11 +      else None
    3.12 +    }
    3.13 +
    3.14  
    3.15    /* current situation */
    3.16  
     4.1 --- a/src/Tools/jEdit/src/plugin.scala	Sat Aug 15 17:38:20 2015 +0200
     4.2 +++ b/src/Tools/jEdit/src/plugin.scala	Sat Aug 15 18:59:31 2015 +0200
     4.3 @@ -221,9 +221,10 @@
     4.4  
     4.5              val aux_files =
     4.6                if (PIDE.options.bool("jedit_auto_resolve")) {
     4.7 -                val snapshot = PIDE.snapshot(view)
     4.8 -                if (snapshot.is_outdated) Nil
     4.9 -                else snapshot.version.nodes.undefined_blobs.map(_.node)
    4.10 +                PIDE.editor.stable_tip_version() match {
    4.11 +                  case Some(version) => version.nodes.undefined_blobs.map(_.node)
    4.12 +                  case None => Nil
    4.13 +                }
    4.14                }
    4.15                else Nil
    4.16