src/Tools/VSCode/src/protocol.scala

   }
 
 
   /* decorations */
 
+  object Decorations
+  {
+    val bad = "bad"
+  }
+
   sealed case class DecorationOptions(range: Line.Range, hover_message: List[MarkedString])
   {
     def json: JSON.T =
       Map("range" -> Range(range)) ++
       JSON.optional("hoverMessage" ->
         (if (hover_message.isEmpty) None else Some(hover_message.map(_.json))))
   }
 
-  object Decoration
-  {
-    def apply(file: JFile, typ: String, content: List[DecorationOptions]): JSON.T =
+  sealed case class Decoration(typ: String, content: List[DecorationOptions])
+  {
+    def json(file: JFile): JSON.T =
       Notification("PIDE/decoration",
         Map("uri" -> Url.print_file(file), "type" -> typ, "content" -> content.map(_.json)))
   }
 }