# HG changeset patch
# User wenzelm
# Date 1489504807 -3600
# Node ID ca571c8c0788a6763a39ec7c719da82bfc905a57
# Parent  4957c7ad92fc16f0fecef7a2b9810ff088ea64c4
avoid race condition between current_state().stable_tip_version and model.rendering();

diff -r 4957c7ad92fc -r ca571c8c0788 src/Tools/VSCode/src/server.scala
--- a/src/Tools/VSCode/src/server.scala	Tue Mar 14 15:19:33 2017 +0100
+++ b/src/Tools/VSCode/src/server.scala	Tue Mar 14 16:20:07 2017 +0100
@@ -163,8 +163,7 @@
   private val delay_output: Standard_Thread.Delay =
     Standard_Thread.delay_last(options.seconds("vscode_output_delay"), channel.Error_Logger)
     {
-      if (session.current_state().stable_tip_version.isEmpty) delay_output.invoke()
-      else resources.flush_output(channel)
+      if (resources.flush_output(channel)) delay_output.invoke()
     }
 
   private val prover_output =
diff -r 4957c7ad92fc -r ca571c8c0788 src/Tools/VSCode/src/vscode_resources.scala
--- a/src/Tools/VSCode/src/vscode_resources.scala	Tue Mar 14 15:19:33 2017 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Tue Mar 14 16:20:07 2017 +0100
@@ -231,15 +231,19 @@
   def update_output(changed_nodes: Traversable[JFile]): Unit =
     state.change(st => st.copy(pending_output = st.pending_output ++ changed_nodes))
 
-  def flush_output(channel: Channel)
+  def flush_output(channel: Channel): Boolean =
   {
-    state.change(st =>
+    state.change_result(st =>
       {
+        val (postponed, flushed) =
+          (for {
+            file <- st.pending_output.iterator
+            model <- st.models.get(file)
+          } yield (file, model, model.rendering())).toList.partition(_._3.snapshot.is_outdated)
+
         val changed_iterator =
           for {
-            file <- st.pending_output.iterator
-            model <- st.models.get(file)
-            rendering = model.rendering()
+            (file, model, rendering) <- flushed.iterator
             (changed_diags, changed_decos, model1) = model.publish(rendering)
             if changed_diags.isDefined || changed_decos.isDefined
           }
@@ -252,9 +256,11 @@
             }
             (file, model1)
           }
-        st.copy(
-          models = st.models ++ changed_iterator,
-          pending_output = Set.empty)
+
+        (postponed.nonEmpty,
+          st.copy(
+            models = st.models ++ changed_iterator,
+            pending_output = postponed.map(_._1).toSet))
       }
     )
   }