author | wenzelm |
Wed, 29 Jul 2015 14:04:19 +0200 | |
changeset 60831 | 5b99a334fd4c |
parent 60830 | f56e189350b2 |
child 60832 | 1cdc63224ed3 |
--- 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 } }