1.1 --- a/src/Pure/PIDE/markup.scala	Tue Dec 23 16:00:38 2014 +0100
     1.2 +++ b/src/Pure/PIDE/markup.scala	Tue Dec 23 20:46:42 2014 +0100
     1.3 @@ -311,7 +311,6 @@
     1.4    val SUBGOALS = "subgoals"
     1.5    val PROOF_STATE = "proof_state"
     1.6  
     1.7 -  val STATE = "state"
     1.8    val GOAL = "goal"
     1.9    val SUBGOAL = "subgoal"
    1.10  
    1.11 @@ -352,6 +351,8 @@
    1.12    val REPORT = "report"
    1.13    val RESULT = "result"
    1.14    val WRITELN = "writeln"
    1.15 +  val STATE = "state"
    1.16 +  val INFORMATION = "information"
    1.17    val TRACING = "tracing"
    1.18    val WARNING = "warning"
    1.19    val ERROR = "error"
    1.20 @@ -362,13 +363,20 @@
    1.21    val EXIT = "exit"
    1.22  
    1.23    val WRITELN_MESSAGE = "writeln_message"
    1.24 +  val STATE_MESSAGE = "state_message"
    1.25 +  val INFORMATION_MESSAGE = "information_message"
    1.26    val TRACING_MESSAGE = "tracing_message"
    1.27    val WARNING_MESSAGE = "warning_message"
    1.28    val ERROR_MESSAGE = "error_message"
    1.29  
    1.30 -  val messages =
    1.31 -    Map(WRITELN -> WRITELN_MESSAGE, TRACING -> TRACING_MESSAGE,
    1.32 -        WARNING -> WARNING_MESSAGE, ERROR -> ERROR_MESSAGE)
    1.33 +  val messages = Map(
    1.34 +    WRITELN -> WRITELN_MESSAGE,
    1.35 +    STATE -> STATE_MESSAGE,
    1.36 +    INFORMATION -> INFORMATION_MESSAGE,
    1.37 +    TRACING -> TRACING_MESSAGE,
    1.38 +    WARNING -> WARNING_MESSAGE,
    1.39 +    ERROR -> ERROR_MESSAGE)
    1.40 +
    1.41    val message: String => String = messages.withDefault((s: String) => s)
    1.42  
    1.43    val Return_Code = new Properties.Int("return_code")
    1.44 @@ -380,7 +388,6 @@
    1.45    val BAD = "bad"
    1.46  
    1.47    val INTENSIFY = "intensify"
    1.48 -  val INFORMATION = "information"
    1.49  
    1.50  
    1.51    /* active areas */