src/Pure/PIDE/markup.scala
changeset 50501 6f41f1646617
parent 50500 c94bba7906d2
child 50503 50f141b34bb7
     1.1 --- a/src/Pure/PIDE/markup.scala	Thu Dec 13 13:52:18 2012 +0100
     1.2 +++ b/src/Pure/PIDE/markup.scala	Thu Dec 13 17:29:23 2012 +0100
     1.3 @@ -264,8 +264,7 @@
     1.4  
     1.5    val message: String => String =
     1.6      Map(WRITELN -> WRITELN_MESSAGE, TRACING -> TRACING_MESSAGE,
     1.7 -        WARNING -> WARNING_MESSAGE, ERROR -> ERROR_MESSAGE)
     1.8 -      .withDefault((name: String) => name + "_message")
     1.9 +        WARNING -> WARNING_MESSAGE, ERROR -> ERROR_MESSAGE).withDefault((s: String) => s)
    1.10  
    1.11    val Return_Code = new Properties.Int("return_code")
    1.12