src/Pure/General/markup.scala

--- a/src/Pure/General/markup.scala	Mon Jul 11 15:56:30 2011 +0200
+++ b/src/Pure/General/markup.scala	Mon Jul 11 16:48:02 2011 +0200
@@ -333,6 +333,22 @@
   val READY = "ready"
 
 
+  /* raw message functions */
+
+  val FUNCTION = "function"
+  val Function = new Property(FUNCTION)
+
+  val INVOKE_SCALA = "invoke_scala"
+  object Invoke_Scala
+  {
+    def unapply(props: List[(String, String)]): Option[(String, String)] =
+      props match {
+        case List((FUNCTION, INVOKE_SCALA), (NAME, name), (ID, id)) => Some((name, id))
+        case _ => None
+      }
+  }
+
+
   /* system data */
 
   val Data = Markup("data", Nil)