src/Pure/PIDE/markup.scala
changeset 59203 5f0bd5afc16d
parent 59186 45e31a196b57
child 59364 3b5da177ae6b
--- a/src/Pure/PIDE/markup.scala	Tue Dec 30 14:11:06 2014 +0100
+++ b/src/Pure/PIDE/markup.scala	Tue Dec 30 23:45:03 2014 +0100
@@ -353,6 +353,7 @@
   val INFORMATION = "information"
   val TRACING = "tracing"
   val WARNING = "warning"
+  val LEGACY = "legacy"
   val ERROR = "error"
   val PROTOCOL = "protocol"
   val SYSTEM = "system"
@@ -365,6 +366,7 @@
   val INFORMATION_MESSAGE = "information_message"
   val TRACING_MESSAGE = "tracing_message"
   val WARNING_MESSAGE = "warning_message"
+  val LEGACY_MESSAGE = "legacy_message"
   val ERROR_MESSAGE = "error_message"
 
   val messages = Map(
@@ -373,14 +375,13 @@
     INFORMATION -> INFORMATION_MESSAGE,
     TRACING -> TRACING_MESSAGE,
     WARNING -> WARNING_MESSAGE,
+    LEGACY -> LEGACY_MESSAGE,
     ERROR -> ERROR_MESSAGE)
 
   val message: String => String = messages.withDefault((s: String) => s)
 
   val Return_Code = new Properties.Int("return_code")
 
-  val LEGACY = "legacy"
-
   val NO_REPORT = "no_report"
 
   val BAD = "bad"