src/Pure/System/isabelle_process.scala
changeset 44732 c58b69d888ac
parent 44705 089fcaf94c00
child 44733 329320fc88df
     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