# HG changeset patch
# User wenzelm
# Date 1483453292 -3600
# Node ID cd545bec3fd016a2db8c7a1f20bef489a13a9acf
# Parent  ae97a5afffcc055fa2bac17762ee96edb1e6bad2
clarified message severity, based on empirical observation of VSCode 1.8.1;

diff -r ae97a5afffcc -r cd545bec3fd0 src/Tools/VSCode/src/protocol.scala
--- 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
diff -r ae97a5afffcc -r cd545bec3fd0 src/Tools/VSCode/src/vscode_rendering.scala
--- 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,