pass raw messages through xml_cache actor, which is important to retain ordering of results (e.g. read_command reports before assign, cf. 383c9d758a56);
authorwenzelm
Sun Sep 04 14:29:15 2011 +0200 (2011-09-04 ago)
changeset 44697b99dfee76538
parent 44696 4e99277c81f2
child 44698 0385292321a0
child 44707 487ae6317f7b
pass raw messages through xml_cache actor, which is important to retain ordering of results (e.g. read_command reports before assign, cf. 383c9d758a56);
src/Pure/General/xml.scala
src/Pure/System/isabelle_process.scala
     1.1 --- a/src/Pure/General/xml.scala	Sun Sep 04 08:43:06 2011 +0200
     1.2 +++ b/src/Pure/General/xml.scala	Sun Sep 04 14:29:15 2011 +0200
     1.3 @@ -159,6 +159,7 @@
     1.4            case Cache_Markup(x, f) => f(cache_markup(x))
     1.5            case Cache_Tree(x, f) => f(cache_tree(x))
     1.6            case Cache_Body(x, f) => f(cache_body(x))
     1.7 +          case Cache_Ignore(x, f) => f(x)
     1.8            case bad => System.err.println("XML.cache_actor: ignoring bad input " + bad)
     1.9          }
    1.10        }
    1.11 @@ -168,12 +169,14 @@
    1.12      private case class Cache_Markup(x: Markup, f: Markup => Unit)
    1.13      private case class Cache_Tree(x: XML.Tree, f: XML.Tree => Unit)
    1.14      private case class Cache_Body(x: XML.Body, f: XML.Body => Unit)
    1.15 +    private case class Cache_Ignore[A](x: A, f: A => Unit)
    1.16  
    1.17      // main methods
    1.18      def cache_string(x: String)(f: String => Unit) { cache_actor ! Cache_String(x, f) }
    1.19      def cache_markup(x: Markup)(f: Markup => Unit) { cache_actor ! Cache_Markup(x, f) }
    1.20      def cache_tree(x: XML.Tree)(f: XML.Tree => Unit) { cache_actor ! Cache_Tree(x, f) }
    1.21      def cache_body(x: XML.Body)(f: XML.Body => Unit) { cache_actor ! Cache_Body(x, f) }
    1.22 +    def cache_ignore[A](x: A)(f: A => Unit) { cache_actor ! Cache_Ignore(x, f) }
    1.23    }
    1.24  
    1.25  
     2.1 --- a/src/Pure/System/isabelle_process.scala	Sun Sep 04 08:43:06 2011 +0200
     2.2 +++ b/src/Pure/System/isabelle_process.scala	Sun Sep 04 14:29:15 2011 +0200
     2.3 @@ -99,7 +99,8 @@
     2.4    {
     2.5      if (kind == Markup.INIT) rm_fifos()
     2.6      if (kind == Markup.RAW)
     2.7 -      receiver ! new Result(XML.Elem(Markup(kind, props), body))
     2.8 +      xml_cache.cache_ignore(
     2.9 +        new Result(XML.Elem(Markup(kind, props), body)))((result: Result) => receiver ! result)
    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) =>