--- a/src/Tools/VSCode/src/protocol.scala Tue Jan 03 15:07:50 2017 +0100
+++ b/src/Tools/VSCode/src/protocol.scala Tue Jan 03 15:21:32 2017 +0100
@@ -329,10 +329,10 @@
object DiagnosticSeverity
{
- val Error = 0
- val Warning = 1
- val Information = 2
- val Hint = 3
+ val Error = 1
+ val Warning = 2
+ val Information = 3
+ val Hint = 4
}
object PublishDiagnostics
--- a/src/Tools/VSCode/src/vscode_rendering.scala Tue Jan 03 15:07:50 2017 +0100
+++ b/src/Tools/VSCode/src/vscode_rendering.scala Tue Jan 03 15:21:32 2017 +0100
@@ -16,7 +16,7 @@
private val message_severity =
Map(
- Markup.WRITELN -> Protocol.DiagnosticSeverity.Hint,
+ Markup.WRITELN -> Protocol.DiagnosticSeverity.Information,
Markup.INFORMATION -> Protocol.DiagnosticSeverity.Information,
Markup.WARNING -> Protocol.DiagnosticSeverity.Warning,
Markup.LEGACY -> Protocol.DiagnosticSeverity.Warning,