more abstract receiver interface;
authorwenzelm
Tue Sep 06 10:27:04 2011 +0200 (2011-09-06 ago)
changeset 44732c58b69d888ac
parent 44731 8f7b3a89fc15
child 44733 329320fc88df
more abstract receiver interface;
src/Pure/System/isabelle_process.scala
src/Pure/System/session.scala
     1.1 --- a/src/Pure/System/isabelle_process.scala	Tue Sep 06 10:16:12 2011 +0200
     1.2 +++ b/src/Pure/System/isabelle_process.scala	Tue Sep 06 10:27:04 2011 +0200
     1.3 @@ -75,22 +75,21 @@
     1.4  }
     1.5  
     1.6  
     1.7 -class Isabelle_Process(timeout: Time, receiver: Actor, args: String*)
     1.8 +class Isabelle_Process(timeout: Time, receiver: Isabelle_Process.Message => Unit, args: String*)
     1.9  {
    1.10    import Isabelle_Process._
    1.11  
    1.12  
    1.13    /* demo constructor */
    1.14  
    1.15 -  def this(args: String*) =
    1.16 -    this(Time.seconds(10), actor { loop { react { case res => Console.println(res) } } }, args: _*)
    1.17 +  def this(args: String*) = this(Time.seconds(10), Console.println(_), args: _*)
    1.18  
    1.19  
    1.20    /* results */
    1.21  
    1.22    private def system_result(text: String)
    1.23    {
    1.24 -    receiver ! new Result(XML.Elem(Markup(Markup.SYSTEM, Nil), List(XML.Text(text))))
    1.25 +    receiver(new Result(XML.Elem(Markup(Markup.SYSTEM, Nil), List(XML.Text(text)))))
    1.26    }
    1.27  
    1.28    private val xml_cache = new XML.Cache()
    1.29 @@ -99,10 +98,10 @@
    1.30    {
    1.31      if (kind == Markup.INIT) rm_fifos()
    1.32      if (kind == Markup.RAW)
    1.33 -      receiver ! new Result(XML.Elem(Markup(kind, props), body))
    1.34 +      receiver(new Result(XML.Elem(Markup(kind, props), body)))
    1.35      else {
    1.36        val msg = XML.Elem(Markup(kind, props), Isar_Document.clean_message(body))
    1.37 -      receiver ! new Result(xml_cache.cache_tree(msg).asInstanceOf[XML.Elem])
    1.38 +      receiver(new Result(xml_cache.cache_tree(msg).asInstanceOf[XML.Elem]))
    1.39      }
    1.40    }
    1.41  
    1.42 @@ -399,7 +398,7 @@
    1.43  
    1.44    def input(name: String, args: String*): Unit =
    1.45    {
    1.46 -    receiver ! new Input(name, args.toList)
    1.47 +    receiver(new Input(name, args.toList))
    1.48      input_bytes(name, args.map(Standard_System.string_bytes): _*)
    1.49    }
    1.50  
     2.1 --- a/src/Pure/System/session.scala	Tue Sep 06 10:16:12 2011 +0200
     2.2 +++ b/src/Pure/System/session.scala	Tue Sep 06 10:27:04 2011 +0200
     2.3 @@ -145,6 +145,7 @@
     2.4    private val (_, session_actor) = Simple_Thread.actor("session_actor", daemon = true)
     2.5    {
     2.6      val this_actor = self
     2.7 +    def receiver(msg: Isabelle_Process.Message) { this_actor ! msg }
     2.8      var prover: Option[Isabelle_Process with Isar_Document] = None
     2.9  
    2.10      var prune_next = System.currentTimeMillis() + prune_delay.ms
    2.11 @@ -371,7 +372,7 @@
    2.12          case Start(timeout, args) if prover.isEmpty =>
    2.13            if (phase == Session.Inactive || phase == Session.Failed) {
    2.14              phase = Session.Startup
    2.15 -            prover = Some(new Isabelle_Process(timeout, this_actor, args:_*) with Isar_Document)
    2.16 +            prover = Some(new Isabelle_Process(timeout, receiver _, args:_*) with Isar_Document)
    2.17            }
    2.18  
    2.19          case Stop =>