support for diagnostics;

--- a/src/Tools/VSCode/src/channel.scala	Mon Dec 26 15:31:13 2016 +0100
+++ b/src/Tools/VSCode/src/channel.scala	Tue Dec 27 16:47:33 2016 +0100
@@ -99,4 +99,10 @@
     display_message(Protocol.MessageType.Warning, message, show)
   def writeln(message: String, show: Boolean = true): Unit =
     display_message(Protocol.MessageType.Info, message, show)
+
+
+  /* diagnostics */
+
+  def diagnostics(uri: String, diagnostics: List[Protocol.Diagnostic]): Unit =
+    write(Protocol.PublishDiagnostics(uri, diagnostics))
 }

--- a/src/Tools/VSCode/src/protocol.scala	Mon Dec 26 15:31:13 2016 +0100
+++ b/src/Tools/VSCode/src/protocol.scala	Tue Dec 27 16:47:33 2016 +0100
@@ -311,4 +311,43 @@
     def reply(id: Id, result: List[Line.Node_Range]): JSON.T =
       ResponseMessage(id, Some(result.map(Location.apply(_))))
   }
+
+
+  /* diagnostics */
+
+  object Diagnostic
+  {
+    def message(range: Line.Range, msg: String, severity: Int): Diagnostic =
+      Diagnostic(range, msg, severity = Some(severity))
+
+    val error: (Line.Range, String) => Diagnostic = message(_, _, DiagnosticSeverity.Error)
+    val warning: (Line.Range, String) => Diagnostic = message(_, _, DiagnosticSeverity.Warning)
+    val information: (Line.Range, String) => Diagnostic = message(_, _, DiagnosticSeverity.Information)
+    val hint: (Line.Range, String) => Diagnostic = message(_, _, DiagnosticSeverity.Hint)
+  }
+
+  sealed case class Diagnostic(range: Line.Range, message: String,
+    severity: Option[Int] = None, code: Option[Int] = None, source: Option[String] = None)
+  {
+    def json: JSON.T =
+      Message.empty + ("range" -> Range(range)) + ("message" -> message) ++
+      (severity match { case Some(x) => Map("severity" -> x) case None => Map.empty }) ++
+      (code match { case Some(x) => Map("code" -> x) case None => Map.empty }) ++
+      (source match { case Some(x) => Map("source" -> x) case None => Map.empty })
+  }
+
+  object DiagnosticSeverity
+  {
+    val Error = 1
+    val Warning = 2
+    val Information = 3
+    val Hint = 4
+  }
+
+  object PublishDiagnostics
+  {
+    def apply(uri: String, diagnostics: List[Diagnostic]): JSON.T =
+      Notification("textDocument/publishDiagnostics",
+        Map("uri" -> uri, "diagnostics" -> diagnostics.map(_.json)))
+  }
 }