publish decorations like diagnostics;
Markup.BAD is decoration, not error message;

--- a/src/Tools/VSCode/extension/src/decorations.ts	Fri Mar 03 19:33:52 2017 +0100
+++ b/src/Tools/VSCode/extension/src/decorations.ts	Fri Mar 03 21:51:04 2017 +0100
@@ -9,7 +9,7 @@
 
 export interface Decorations
 {
-  test: TextEditorDecorationType
+  bad: TextEditorDecorationType
 }
 
 export let types: Readonly<Decorations>
@@ -26,7 +26,7 @@
   if (!types)
     types =
     {
-      test: decoration({ backgroundColor: 'rgba(255,0,0,0.3)' })
+      bad: decoration({ backgroundColor: 'rgba(255, 106, 106, 0.4)' })
     }
 }
 

--- a/src/Tools/VSCode/src/channel.scala	Fri Mar 03 19:33:52 2017 +0100
+++ b/src/Tools/VSCode/src/channel.scala	Fri Mar 03 21:51:04 2017 +0100
@@ -112,10 +112,4 @@
       override def theory(session: String, theory: String): Unit =
         if (verbose) echo(session + ": theory " + theory)
     }
-
-
-  /* diagnostics */
-
-  def diagnostics(file: JFile, diagnostics: List[Protocol.Diagnostic]): Unit =
-    write(Protocol.PublishDiagnostics(file, diagnostics))
 }

--- a/src/Tools/VSCode/src/document_model.scala	Fri Mar 03 19:33:52 2017 +0100
+++ b/src/Tools/VSCode/src/document_model.scala	Fri Mar 03 21:51:04 2017 +0100
@@ -14,6 +14,13 @@
 
 object Document_Model
 {
+  /* decorations */
+
+  sealed case class Decoration(typ: String, content: List[Text.Info[XML.Body]])
+
+
+  /* content */
+
   sealed case class Content(doc: Line.Document)
   {
     def text_range: Text.Range = doc.text_range
@@ -43,7 +50,8 @@
   node_required: Boolean = false,
   last_perspective: Document.Node.Perspective_Text = Document.Node.no_perspective_text,
   pending_edits: List[Text.Edit] = Nil,
-  published_diagnostics: List[Text.Info[Command.Results]] = Nil) extends Document.Model
+  published_diagnostics: List[Text.Info[Command.Results]] = Nil,
+  published_decorations: List[Document_Model.Decoration] = Nil) extends Document.Model
 {
   /* external file */
 
@@ -111,14 +119,22 @@
   }
 
 
-  /* diagnostics */
+  /* publish annotations */
 
-  def publish_diagnostics(rendering: VSCode_Rendering)
-    : Option[(List[Text.Info[Command.Results]], Document_Model)] =
+  def publish(rendering: VSCode_Rendering)
+    : Option[((List[Text.Info[Command.Results]], List[Document_Model.Decoration]), Document_Model)] =
   {
     val diagnostics = rendering.diagnostics
-    if (diagnostics == published_diagnostics) None
-    else Some(diagnostics, copy(published_diagnostics = diagnostics))
+    val decorations = rendering.decorations
+    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))
+    }
   }
 
 

--- a/src/Tools/VSCode/src/protocol.scala	Fri Mar 03 19:33:52 2017 +0100
+++ b/src/Tools/VSCode/src/protocol.scala	Fri Mar 03 21:51:04 2017 +0100
@@ -407,6 +407,11 @@
 
   /* decorations */
 
+  object Decorations
+  {
+    val bad = "bad"
+  }
+
   sealed case class DecorationOptions(range: Line.Range, hover_message: List[MarkedString])
   {
     def json: JSON.T =
@@ -415,9 +420,9 @@
         (if (hover_message.isEmpty) None else Some(hover_message.map(_.json))))
   }
 
-  object Decoration
+  sealed case class Decoration(typ: String, content: List[DecorationOptions])
   {
-    def apply(file: JFile, typ: String, content: List[DecorationOptions]): JSON.T =
+    def json(file: JFile): JSON.T =
       Notification("PIDE/decoration",
         Map("uri" -> Url.print_file(file), "type" -> typ, "content" -> content.map(_.json)))
   }

--- a/src/Tools/VSCode/src/vscode_rendering.scala	Fri Mar 03 19:33:52 2017 +0100
+++ b/src/Tools/VSCode/src/vscode_rendering.scala	Fri Mar 03 21:51:04 2017 +0100
@@ -23,15 +23,15 @@
       Markup.INFORMATION -> Protocol.DiagnosticSeverity.Information,
       Markup.WARNING -> Protocol.DiagnosticSeverity.Warning,
       Markup.LEGACY -> Protocol.DiagnosticSeverity.Warning,
-      Markup.ERROR -> Protocol.DiagnosticSeverity.Error,
-      Markup.BAD -> Protocol.DiagnosticSeverity.Error)
+      Markup.ERROR -> Protocol.DiagnosticSeverity.Error)
 
 
   /* markup elements */
 
   private val diagnostics_elements =
-    Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING, Markup.LEGACY, Markup.ERROR,
-      Markup.BAD)
+    Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING, Markup.LEGACY, Markup.ERROR)
+
+  private val bad_elements = Markup.Elements(Markup.BAD)
 
   private val hyperlink_elements =
     Markup.Elements(Markup.ENTITY, Markup.PATH, Markup.POSITION, Markup.CITATION)
@@ -94,6 +94,30 @@
   }
 
 
+  /* decorations */
+
+  def decorations: List[Document_Model.Decoration] =
+    List(Document_Model.Decoration(Protocol.Decorations.bad, decorations_bad))
+
+  def decorations_bad: List[Text.Info[XML.Body]] =
+    snapshot.select(model.content.text_range, VSCode_Rendering.bad_elements, _ =>
+      {
+        case Text.Info(_, XML.Elem(_, body)) => Some(body)
+      })
+
+  def decoration_output(decoration: Document_Model.Decoration): Protocol.Decoration =
+  {
+    val content =
+      for (Text.Info(text_range, body) <- decoration.content)
+      yield {
+        val range = model.content.doc.range(text_range)
+        val msg = resources.output_pretty(body, diagnostics_margin)
+        Protocol.DecorationOptions(range, if (msg == "") Nil else List(Protocol.MarkedString(msg)))
+      }
+    Protocol.Decoration(decoration.typ, content)
+  }
+
+
   /* tooltips */
 
   def tooltip_margin: Int = options.int("vscode_tooltip_margin")

--- a/src/Tools/VSCode/src/vscode_resources.scala	Fri Mar 03 19:33:52 2017 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Fri Mar 03 21:51:04 2017 +0100
@@ -236,9 +236,16 @@
             file <- st.pending_output.iterator
             model <- st.models.get(file)
             rendering = model.rendering()
-            (diagnostics, model1) <- model.publish_diagnostics(rendering)
-          } yield {
-            channel.diagnostics(file, rendering.diagnostics_output(diagnostics))
+            ((diagnostics, decorations), model1) <- model.publish(rendering)
+          }
+          yield {
+            if (diagnostics.nonEmpty)
+              channel.write(
+                Protocol.PublishDiagnostics(file, rendering.diagnostics_output(diagnostics)))
+
+            for (decoration <- decorations)
+              channel.write(rendering.decoration_output(decoration).json(file))
+
             (file, model1)
           }
         st.copy(