src/Pure/General/markup.scala

--- a/src/Pure/General/markup.scala	Sat Aug 07 22:09:52 2010 +0200
+++ b/src/Pure/General/markup.scala	Sat Aug 07 22:43:57 2010 +0200
@@ -183,7 +183,7 @@
 
   /* interactive documents */
 
-  val ASSIGN = "assign"
+  val Assign = Markup("assign", Nil)
   val EDIT = "edit"
 
 
@@ -207,12 +207,12 @@
   val SIGNAL = "signal"
   val EXIT = "exit"
 
-  val READY = "ready"
+  val Ready = Markup("ready", Nil)
 
 
   /* system data */
 
-  val DATA = "data"
+  val Data = Markup("data", Nil)
 }
 
 sealed case class Markup(name: String, properties: List[(String, String)])