# HG changeset patch
# User wenzelm
# Date 1488738459 -3600
# Node ID db6cc23fcf3319147ec4ee37d437a015f1a0b735
# Parent  a7bedf94e71cf2e85d64c48b2bbccad437c3fa76
proper reset of published decorations: initial value is Nil, afterwards it is a list of canonical length and order;

diff -r a7bedf94e71c -r db6cc23fcf33 src/Tools/VSCode/src/document_model.scala
--- a/src/Tools/VSCode/src/document_model.scala	Sun Mar 05 18:59:39 2017 +0100
+++ b/src/Tools/VSCode/src/document_model.scala	Sun Mar 05 19:27:39 2017 +0100
@@ -125,13 +125,15 @@
     (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
+    val decorations =
+      if (node_visible) rendering.decorations
+      else { for (deco <- published_decorations) yield Document_Model.Decoration(deco.typ, Nil) }
 
     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 if (published_decorations.isEmpty) Some(decorations)
       else Some(for { (a, b) <- decorations zip published_decorations if a != b } yield a)
 
     (changed_diagnostics, changed_decorations,
diff -r a7bedf94e71c -r db6cc23fcf33 src/Tools/VSCode/src/vscode_rendering.scala
--- a/src/Tools/VSCode/src/vscode_rendering.scala	Sun Mar 05 18:59:39 2017 +0100
+++ b/src/Tools/VSCode/src/vscode_rendering.scala	Sun Mar 05 19:27:39 2017 +0100
@@ -128,7 +128,7 @@
     Document_Model.Decoration("hover_message", content)
   }
 
-  def decorations: List[Document_Model.Decoration] =
+  def decorations: List[Document_Model.Decoration] = // list of canonical length and order
     hover_message ::
     VSCode_Rendering.color_decorations("background_", Rendering.Color.background,
       background(model.content.text_range, Set.empty)) :::