--- a/src/Tools/VSCode/src/protocol.scala Wed Dec 28 17:35:12 2016 +0100
+++ b/src/Tools/VSCode/src/protocol.scala Wed Dec 28 17:38:12 2016 +0100
@@ -315,17 +315,6 @@
/* 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)
{