diff -r dd7dcb9b2637 -r 2b61c5e27399 src/Pure/General/markup.scala
--- a/src/Pure/General/markup.scala	Tue Aug 10 12:09:53 2010 +0200
+++ b/src/Pure/General/markup.scala	Tue Aug 10 12:29:11 2010 +0200
@@ -203,6 +203,7 @@
   val ERROR = "error"
   val DEBUG = "debug"
   val SYSTEM = "system"
+  val INPUT = "input"
   val STDIN = "stdin"
   val STDOUT = "stdout"
   val SIGNAL = "signal"