tuned;
authorwenzelm
Wed Jul 29 14:04:19 2015 +0200 (2015-07-29)
changeset 608315b99a334fd4c
parent 60830 f56e189350b2
child 60832 1cdc63224ed3
tuned;
src/Pure/PIDE/markup.scala
     1.1 --- a/src/Pure/PIDE/markup.scala	Wed Jul 29 13:34:04 2015 +0200
     1.2 +++ b/src/Pure/PIDE/markup.scala	Wed Jul 29 14:04:19 2015 +0200
     1.3 @@ -485,7 +485,7 @@
     1.4    {
     1.5      def unapply(props: Properties.T): Option[String] =
     1.6        props match {
     1.7 -        case List((FUNCTION, BUILD_THEORIES_RESULT), ("id", id)) => Some(id)
     1.8 +        case List((FUNCTION, BUILD_THEORIES_RESULT), (ID, id)) => Some(id)
     1.9          case _ => None
    1.10        }
    1.11    }