# HG changeset patch
# User wenzelm
# Date 1483778577 -3600
# Node ID 899c69bad0a9dd5eab6ef23e25bfc94a8af63380
# Parent  c7693244672e9cba6d33321961ff4e8d5a1b94ff
tuned;

diff -r c7693244672e -r 899c69bad0a9 src/Pure/PIDE/document.scala
--- 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
   }
 
 
diff -r c7693244672e -r 899c69bad0a9 src/Tools/VSCode/src/document_model.scala
--- 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)
diff -r c7693244672e -r 899c69bad0a9 src/Tools/VSCode/src/vscode_resources.scala
--- 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