tuned;
authorwenzelm
Sat, 07 Jan 2017 09:42:57 +0100
changeset 64815 899c69bad0a9
parent 64814 c7693244672e
child 64816 e306cab8edf9
tuned;
src/Pure/PIDE/document.scala
src/Tools/VSCode/src/document_model.scala
src/Tools/VSCode/src/vscode_resources.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
   }
 
 
--- 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