src/Pure/PIDE/xml.scala
changeset 44705 089fcaf94c00
parent 44704 528d635ef6f0
child 44721 ba478c3f7255
     1.1 --- a/src/Pure/PIDE/xml.scala	Sun Sep 04 19:06:45 2011 +0200
     1.2 +++ b/src/Pure/PIDE/xml.scala	Sun Sep 04 19:12:06 2011 +0200
     1.3 @@ -151,12 +151,10 @@
     1.4          }
     1.5  
     1.6      // main methods
     1.7 -    // FIXME simplify signatures
     1.8 -    def cache_string(x: String)(f: String => Unit): Unit = f(synchronized { _cache_string(x) })
     1.9 -    def cache_markup(x: Markup)(f: Markup => Unit): Unit = f(synchronized { _cache_markup(x) })
    1.10 -    def cache_tree(x: XML.Tree)(f: XML.Tree => Unit): Unit = f(synchronized { _cache_tree(x) })
    1.11 -    def cache_body(x: XML.Body)(f: XML.Body => Unit): Unit = f(synchronized { _cache_body(x) })
    1.12 -    def cache_ignore[A](x: A)(f: A => Unit): Unit = f(x)
    1.13 +    def cache_string(x: String): String = synchronized { _cache_string(x) }
    1.14 +    def cache_markup(x: Markup): Markup = synchronized { _cache_markup(x) }
    1.15 +    def cache_tree(x: XML.Tree): XML.Tree = synchronized { _cache_tree(x) }
    1.16 +    def cache_body(x: XML.Body): XML.Body = synchronized { _cache_body(x) }
    1.17    }
    1.18  
    1.19