simplified signatures;

--- a/src/Pure/PIDE/xml.scala	Sun Sep 04 19:06:45 2011 +0200
+++ b/src/Pure/PIDE/xml.scala	Sun Sep 04 19:12:06 2011 +0200
@@ -151,12 +151,10 @@
         }
 
     // main methods
-    // FIXME simplify signatures
-    def cache_string(x: String)(f: String => Unit): Unit = f(synchronized { _cache_string(x) })
-    def cache_markup(x: Markup)(f: Markup => Unit): Unit = f(synchronized { _cache_markup(x) })
-    def cache_tree(x: XML.Tree)(f: XML.Tree => Unit): Unit = f(synchronized { _cache_tree(x) })
-    def cache_body(x: XML.Body)(f: XML.Body => Unit): Unit = f(synchronized { _cache_body(x) })
-    def cache_ignore[A](x: A)(f: A => Unit): Unit = f(x)
+    def cache_string(x: String): String = synchronized { _cache_string(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) }
   }
 
 

--- a/src/Pure/System/isabelle_process.scala	Sun Sep 04 19:06:45 2011 +0200
+++ b/src/Pure/System/isabelle_process.scala	Sun Sep 04 19:12:06 2011 +0200
@@ -99,12 +99,10 @@
   {
     if (kind == Markup.INIT) rm_fifos()
     if (kind == Markup.RAW)
-      xml_cache.cache_ignore(
-        new Result(XML.Elem(Markup(kind, props), body)))((result: Result) => receiver ! result)
+      receiver ! new Result(XML.Elem(Markup(kind, props), body))
     else {
       val msg = XML.Elem(Markup(kind, props), Isar_Document.clean_message(body))
-      xml_cache.cache_tree(msg)((message: XML.Tree) =>
-        receiver ! new Result(message.asInstanceOf[XML.Elem]))
+      receiver ! new Result(xml_cache.cache_tree(msg).asInstanceOf[XML.Elem])
     }
   }