diff -r ed147003de4b -r 968844caaff9 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)])