--- 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))
}