--- 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"