# HG changeset patch
# User wenzelm
# Date 1438171459 -7200
# Node ID 5b99a334fd4cf91b63f1c8d7c041a41ace5426f2
# Parent  f56e189350b299eeb5c32c425ec01b7dac367a73
tuned;

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
       }
   }