# HG changeset patch
# User wenzelm
# Date 1488717275 -3600
# Node ID 3224a6f7bd6b0c4008f3b13d302cd7803ab9c17e
# Parent  73cd69353f7f9e5a13f46aa278d5704a372b84c2
more robust treatment of pending input/output: these are often correlated;
no decorations for invisible node;

diff -r 73cd69353f7f -r 3224a6f7bd6b src/Tools/VSCode/src/document_model.scala
--- a/src/Tools/VSCode/src/document_model.scala	Sun Mar 05 12:07:36 2017 +0100
+++ b/src/Tools/VSCode/src/document_model.scala	Sun Mar 05 13:34:35 2017 +0100
@@ -125,7 +125,7 @@
     : Option[((List[Text.Info[Command.Results]], List[Document_Model.Decoration]), Document_Model)] =
   {
     val diagnostics = rendering.diagnostics
-    val decorations = rendering.decorations
+    val decorations = if (node_visible) rendering.decorations else Nil
     if (diagnostics == published_diagnostics && decorations == published_decorations) None
     else {
       val new_decorations =
diff -r 73cd69353f7f -r 3224a6f7bd6b src/Tools/VSCode/src/server.scala
--- a/src/Tools/VSCode/src/server.scala	Sun Mar 05 12:07:36 2017 +0100
+++ b/src/Tools/VSCode/src/server.scala	Sun Mar 05 13:34:35 2017 +0100
@@ -124,24 +124,32 @@
   private val file_watcher =
     File_Watcher(sync_documents(_), options.seconds("vscode_load_delay"))
 
-  private def sync_documents(changed: Set[JFile]): Unit =
-    if (resources.sync_models(changed)) delay_input.invoke()
+  private def close_document(file: JFile)
+  {
+    if (resources.close_model(file)) {
+      file_watcher.register_parent(file)
+      if (!sync_documents(Set(file))) {
+        delay_input.invoke()
+        delay_output.invoke()
+      }
+    }
+  }
+
+  private def sync_documents(changed: Set[JFile]): Boolean =
+    if (resources.sync_models(changed)) {
+      delay_input.invoke()
+      delay_output.invoke()
+      true
+    }
+    else false
 
   private def update_document(file: JFile, text: String)
   {
     resources.update_model(session, file, text)
     delay_input.invoke()
+    delay_output.invoke()
   }
 
-  private def close_document(file: JFile)
-  {
-    resources.close_model(file) match {
-      case Some(model) =>
-        file_watcher.register_parent(file)
-        sync_documents(Set(file))
-      case None =>
-    }
-  }
 
 
   /* output to client */
diff -r 73cd69353f7f -r 3224a6f7bd6b src/Tools/VSCode/src/vscode_resources.scala
--- a/src/Tools/VSCode/src/vscode_resources.scala	Sun Mar 05 12:07:36 2017 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Sun Mar 05 13:34:35 2017 +0100
@@ -23,6 +23,11 @@
     pending_input: Set[JFile] = Set.empty,
     pending_output: Set[JFile] = Set.empty)
   {
+    def pending(changed: Traversable[JFile]) =
+      copy(
+        pending_input = pending_input ++ changed,
+        pending_output = pending_output ++ changed)
+
     lazy val document_blobs: Document.Blobs =
       Document.Blobs(
         (for {
@@ -116,16 +121,19 @@
         val model1 = (model.update_text(text) getOrElse model).external(false)
         st.copy(
           models = st.models + (file -> model1),
-          pending_input = st.pending_input + file)
+          pending_input = st.pending_input + file,
+          pending_output = st.pending_output ++
+            (if (model.node_visible == model1.node_visible) None else Some(file)))
       })
   }
 
-  def close_model(file: JFile): Option[Document_Model] =
+  def close_model(file: JFile): Boolean =
     state.change_result(st =>
       st.models.get(file) match {
-        case None => (None, st)
+        case None => (false, st)
         case Some(model) =>
-          (Some(model), st.copy(models = st.models + (file -> model.external(true))))
+          val model1 = model.external(true)
+          (true, st.copy(models = st.models + (file -> model1)).pending(Some(file)))
       })
 
   def sync_models(changed_files: Set[JFile]): Boolean =
@@ -137,12 +145,9 @@
             if changed_files(file) && model.external_file
             text <- read_file_content(file)
             model1 <- model.update_text(text)
-          } yield (file, model1)).toList
+          } yield (file, model1)).toMap
         if (changed_models.isEmpty) (false, st)
-        else (true,
-          st.copy(
-            models = (st.models /: changed_models)(_ + _),
-            pending_input = (st.pending_input /: changed_models.iterator.map(_._1))(_ + _)))
+        else (true, st.copy(models = st.models ++ changed_models).pending(changed_models.keySet))
       })
 
 
@@ -188,15 +193,13 @@
             val model = Document_Model.init(session, node_name)
             val model1 = (model.update_text(text) getOrElse model).external(true)
             (file, model1)
-          }).toList
+          }).toMap
 
         val invoke_input = loaded_models.nonEmpty
         val invoke_load = stable_tip_version.isEmpty
 
         ((invoke_input, invoke_load),
-          st.copy(
-            models = st.models ++ loaded_models,
-            pending_input = st.pending_input ++ loaded_models.iterator.map(_._1)))
+          st.copy(models = st.models ++ loaded_models).pending(loaded_models.keySet))
       })
   }