diff -r 8c3e5fb41139 -r c6a8a05ff0a0 src/Pure/PIDE/xml.scala
--- a/src/Pure/PIDE/xml.scala	Tue Feb 19 17:55:26 2013 +0100
+++ b/src/Pure/PIDE/xml.scala	Tue Feb 19 20:19:21 2013 +0100
@@ -188,6 +188,7 @@
 
     // main methods
     def cache_string(x: String): String = synchronized { _cache_string(x) }
+    def cache_props(x: Properties.T): Properties.T = synchronized { _cache_props(x) }
     def cache_markup(x: Markup): Markup = synchronized { _cache_markup(x) }
     def cache_tree(x: XML.Tree): XML.Tree = synchronized { _cache_tree(x) }
     def cache_body(x: XML.Body): XML.Body = synchronized { _cache_body(x) }