# HG changeset patch # User wenzelm # Date 1482853653 -3600 # Node ID c557279d93f22c582b47b9d5b4d25b2b43f1fdb3 # Parent b5965890e54dc49c2010b6c91a12526fffbaa3d5 support for diagnostics; diff -r b5965890e54d -r c557279d93f2 src/Tools/VSCode/src/channel.scala --- 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)) } diff -r b5965890e54d -r c557279d93f2 src/Tools/VSCode/src/protocol.scala --- 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))) + } }