src/Pure/PIDE/markup.scala
changeset 52111 1fd184eaa310
parent 51818 517f232e867d
child 52563 f9a20c2c3b70
     1.1 --- a/src/Pure/PIDE/markup.scala	Wed May 22 08:46:39 2013 +0200
     1.2 +++ b/src/Pure/PIDE/markup.scala	Wed May 22 14:10:45 2013 +0200
     1.3 @@ -316,19 +316,31 @@
     1.4    val Assign_Execs: Properties.T = List((FUNCTION, "assign_execs"))
     1.5    val Removed_Versions: Properties.T = List((FUNCTION, "removed_versions"))
     1.6  
     1.7 +  object Protocol_Handler
     1.8 +  {
     1.9 +    def unapply(props: Properties.T): Option[(String)] =
    1.10 +      props match {
    1.11 +        case List((FUNCTION, "protocol_handler"), (NAME, name)) => Some(name)
    1.12 +        case _ => None
    1.13 +      }
    1.14 +  }
    1.15 +
    1.16 +  val INVOKE_SCALA = "invoke_scala"
    1.17    object Invoke_Scala
    1.18    {
    1.19      def unapply(props: Properties.T): Option[(String, String)] =
    1.20        props match {
    1.21 -        case List((FUNCTION, "invoke_scala"), (NAME, name), (ID, id)) => Some((name, id))
    1.22 +        case List((FUNCTION, INVOKE_SCALA), (NAME, name), (ID, id)) => Some((name, id))
    1.23          case _ => None
    1.24        }
    1.25    }
    1.26 +
    1.27 +  val CANCEL_SCALA = "cancel_scala"
    1.28    object Cancel_Scala
    1.29    {
    1.30      def unapply(props: Properties.T): Option[String] =
    1.31        props match {
    1.32 -        case List((FUNCTION, "cancel_scala"), (ID, id)) => Some(id)
    1.33 +        case List((FUNCTION, CANCEL_SCALA), (ID, id)) => Some(id)
    1.34          case _ => None
    1.35        }
    1.36    }