--- a/src/Pure/PIDE/markup.scala Tue Aug 06 17:30:09 2013 +0200
+++ b/src/Pure/PIDE/markup.scala Tue Aug 06 21:08:04 2013 +0200
@@ -245,6 +245,8 @@
val FINISHED = "finished"
val FAILED = "failed"
+ val WAITING = "waiting"
+
/* interactive documents */
@@ -283,9 +285,10 @@
val WARNING_MESSAGE = "warning_message"
val ERROR_MESSAGE = "error_message"
- val message: String => String =
+ val messages =
Map(WRITELN -> WRITELN_MESSAGE, TRACING -> TRACING_MESSAGE,
- WARNING -> WARNING_MESSAGE, ERROR -> ERROR_MESSAGE).withDefault((s: String) => s)
+ WARNING -> WARNING_MESSAGE, ERROR -> ERROR_MESSAGE)
+ val message: String => String = messages.withDefault((s: String) => s)
val Return_Code = new Properties.Int("return_code")