publish output more thoroughly;

--- a/src/Tools/VSCode/src/document_model.scala	Sun Mar 05 14:13:58 2017 +0100
+++ b/src/Tools/VSCode/src/document_model.scala	Sun Mar 05 14:33:43 2017 +0100
@@ -121,20 +121,21 @@
 
   /* publish annotations */
 
-  def publish(rendering: VSCode_Rendering)
-    : Option[((List[Text.Info[Command.Results]], List[Document_Model.Decoration]), Document_Model)] =
+  def publish(rendering: VSCode_Rendering):
+    (Option[List[Text.Info[Command.Results]]], Option[List[Document_Model.Decoration]], Document_Model) =
   {
     val diagnostics = rendering.diagnostics
     val decorations = if (node_visible) rendering.decorations else Nil
-    if (diagnostics == published_diagnostics && decorations == published_decorations) None
-    else {
-      val new_decorations =
-        if (decorations.length != published_decorations.length) decorations
-        else for { (a, b) <- decorations zip published_decorations if a != b } yield a
 
-      Some((diagnostics, new_decorations),
-        copy(published_diagnostics = diagnostics, published_decorations = decorations))
-    }
+    val changed_diagnostics =
+      if (diagnostics == published_diagnostics) None else Some(diagnostics)
+    val changed_decorations =
+      if (decorations == published_decorations) None
+      else if (decorations.length != published_decorations.length) Some(decorations)
+      else Some(for { (a, b) <- decorations zip published_decorations if a != b } yield a)
+
+    (changed_diagnostics, changed_decorations,
+      copy(published_diagnostics = diagnostics, published_decorations = decorations))
   }
 
 

--- a/src/Tools/VSCode/src/vscode_resources.scala	Sun Mar 05 14:13:58 2017 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Sun Mar 05 14:33:43 2017 +0100
@@ -233,16 +233,14 @@
             file <- st.pending_output.iterator
             model <- st.models.get(file)
             rendering = model.rendering()
-            ((diagnostics, decorations), model1) <- model.publish(rendering)
+            (changed_diags, changed_decos, model1) = model.publish(rendering)
+            if changed_diags.isDefined || changed_decos.isDefined
           }
           yield {
-            if (diagnostics.nonEmpty)
-              channel.write(
-                Protocol.PublishDiagnostics(file, rendering.diagnostics_output(diagnostics)))
-
-            for (decoration <- decorations)
-              channel.write(rendering.decoration_output(decoration).json(file))
-
+            for (diags <- changed_diags)
+              channel.write(Protocol.PublishDiagnostics(file, rendering.diagnostics_output(diags)))
+            for (decos <- changed_decos; deco <- decos)
+              channel.write(rendering.decoration_output(deco).json(file))
             (file, model1)
           }
         st.copy(