diff -r f56e189350b2 -r 5b99a334fd4c src/Pure/PIDE/markup.scala --- a/src/Pure/PIDE/markup.scala Wed Jul 29 13:34:04 2015 +0200 +++ b/src/Pure/PIDE/markup.scala Wed Jul 29 14:04:19 2015 +0200 @@ -485,7 +485,7 @@ { def unapply(props: Properties.T): Option[String] = props match { - case List((FUNCTION, BUILD_THEORIES_RESULT), ("id", id)) => Some(id) + case List((FUNCTION, BUILD_THEORIES_RESULT), (ID, id)) => Some(id) case _ => None } }