1.1 --- a/src/Pure/PIDE/xml.scala	Tue Feb 19 17:55:26 2013 +0100
     1.2 +++ b/src/Pure/PIDE/xml.scala	Tue Feb 19 20:19:21 2013 +0100
     1.3 @@ -188,6 +188,7 @@
     1.4  
     1.5      // main methods
     1.6      def cache_string(x: String): String = synchronized { _cache_string(x) }
     1.7 +    def cache_props(x: Properties.T): Properties.T = synchronized { _cache_props(x) }
     1.8      def cache_markup(x: Markup): Markup = synchronized { _cache_markup(x) }
     1.9      def cache_tree(x: XML.Tree): XML.Tree = synchronized { _cache_tree(x) }
    1.10      def cache_body(x: XML.Body): XML.Body = synchronized { _cache_body(x) }