simplified signatures;
authorwenzelm
Sun Sep 04 19:12:06 2011 +0200 (2011-09-04 ago)
changeset 44705089fcaf94c00
parent 44704 528d635ef6f0
child 44706 fe319b45315c
simplified signatures;
src/Pure/PIDE/xml.scala
src/Pure/System/isabelle_process.scala
     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  
     2.1 --- a/src/Pure/System/isabelle_process.scala	Sun Sep 04 19:06:45 2011 +0200
     2.2 +++ b/src/Pure/System/isabelle_process.scala	Sun Sep 04 19:12:06 2011 +0200
     2.3 @@ -99,12 +99,10 @@
     2.4    {
     2.5      if (kind == Markup.INIT) rm_fifos()
     2.6      if (kind == Markup.RAW)
     2.7 -      xml_cache.cache_ignore(
     2.8 -        new Result(XML.Elem(Markup(kind, props), body)))((result: Result) => receiver ! result)
     2.9 +      receiver ! new Result(XML.Elem(Markup(kind, props), body))
    2.10      else {
    2.11        val msg = XML.Elem(Markup(kind, props), Isar_Document.clean_message(body))
    2.12 -      xml_cache.cache_tree(msg)((message: XML.Tree) =>
    2.13 -        receiver ! new Result(message.asInstanceOf[XML.Elem]))
    2.14 +      receiver ! new Result(xml_cache.cache_tree(msg).asInstanceOf[XML.Elem])
    2.15      }
    2.16    }
    2.17