src/Pure/PIDE/markup.scala
changeset 59203 5f0bd5afc16d
parent 59186 45e31a196b57
child 59364 3b5da177ae6b
     1.1 --- a/src/Pure/PIDE/markup.scala	Tue Dec 30 14:11:06 2014 +0100
     1.2 +++ b/src/Pure/PIDE/markup.scala	Tue Dec 30 23:45:03 2014 +0100
     1.3 @@ -353,6 +353,7 @@
     1.4    val INFORMATION = "information"
     1.5    val TRACING = "tracing"
     1.6    val WARNING = "warning"
     1.7 +  val LEGACY = "legacy"
     1.8    val ERROR = "error"
     1.9    val PROTOCOL = "protocol"
    1.10    val SYSTEM = "system"
    1.11 @@ -365,6 +366,7 @@
    1.12    val INFORMATION_MESSAGE = "information_message"
    1.13    val TRACING_MESSAGE = "tracing_message"
    1.14    val WARNING_MESSAGE = "warning_message"
    1.15 +  val LEGACY_MESSAGE = "legacy_message"
    1.16    val ERROR_MESSAGE = "error_message"
    1.17  
    1.18    val messages = Map(
    1.19 @@ -373,14 +375,13 @@
    1.20      INFORMATION -> INFORMATION_MESSAGE,
    1.21      TRACING -> TRACING_MESSAGE,
    1.22      WARNING -> WARNING_MESSAGE,
    1.23 +    LEGACY -> LEGACY_MESSAGE,
    1.24      ERROR -> ERROR_MESSAGE)
    1.25  
    1.26    val message: String => String = messages.withDefault((s: String) => s)
    1.27  
    1.28    val Return_Code = new Properties.Int("return_code")
    1.29  
    1.30 -  val LEGACY = "legacy"
    1.31 -
    1.32    val NO_REPORT = "no_report"
    1.33  
    1.34    val BAD = "bad"