--- a/src/Pure/PIDE/document.scala Fri Jan 06 23:25:18 2017 +0100
+++ b/src/Pure/PIDE/document.scala Sat Jan 07 09:42:57 2017 +0100
@@ -471,17 +471,17 @@
trait Model
{
- /*session*/
def session: Session
- def snapshot(): Snapshot
- /*name*/
def node_name: Document.Node.Name
def is_theory: Boolean = node_name.is_theory
override def toString: String = node_name.toString
- /*content*/
+ def node_required: Boolean
def get_blob: Option[Document.Blob]
+
+ def is_stable: Boolean
+ def snapshot(): Snapshot
}
--- a/src/Tools/VSCode/src/document_model.scala Fri Jan 06 23:25:18 2017 +0100
+++ b/src/Tools/VSCode/src/document_model.scala Sat Jan 07 09:42:57 2017 +0100
@@ -85,6 +85,8 @@
/* edits */
+ def is_stable: Boolean = pending_edits.isEmpty
+
def update_text(text: String): Option[Document_Model] =
{
val new_text = Line.normalize(text)
--- a/src/Tools/VSCode/src/vscode_resources.scala Fri Jan 06 23:25:18 2017 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala Sat Jan 07 09:42:57 2017 +0100
@@ -164,7 +164,7 @@
/* auxiliary files */
val stable_tip_version =
- if (st.models.forall({ case (_, model) => model.pending_edits.isEmpty }))
+ if (st.models.forall(entry => entry._2.is_stable))
session.current_state().stable_tip_version
else None