src/Pure/System/isabelle_process.scala
changeset 43661 39fdbd814c7f
parent 43520 cec9b95fa35d
child 43695 5130dfe1b7be
     1.1 --- a/src/Pure/System/isabelle_process.scala	Mon Jul 04 20:18:19 2011 +0200
     1.2 +++ b/src/Pure/System/isabelle_process.scala	Mon Jul 04 22:11:32 2011 +0200
     1.3 @@ -62,7 +62,7 @@
     1.4  }
     1.5  
     1.6  
     1.7 -class Isabelle_Process(system: Isabelle_System, timeout: Time, receiver: Actor, args: String*)
     1.8 +class Isabelle_Process(timeout: Time, receiver: Actor, args: String*)
     1.9  {
    1.10    import Isabelle_Process._
    1.11  
    1.12 @@ -70,8 +70,7 @@
    1.13    /* demo constructor */
    1.14  
    1.15    def this(args: String*) =
    1.16 -    this(Isabelle_System.default, Time.seconds(10),
    1.17 -      actor { loop { react { case res => Console.println(res) } } }, args: _*)
    1.18 +    this(Time.seconds(10), actor { loop { react { case res => Console.println(res) } } }, args: _*)
    1.19  
    1.20  
    1.21    /* results */
    1.22 @@ -93,7 +92,7 @@
    1.23  
    1.24    private def put_result(kind: String, text: String)
    1.25    {
    1.26 -    put_result(kind, Nil, List(XML.Text(system.symbols.decode(text))))
    1.27 +    put_result(kind, Nil, List(XML.Text(Isabelle_System.symbols.decode(text))))
    1.28    }
    1.29  
    1.30  
    1.31 @@ -117,15 +116,16 @@
    1.32  
    1.33    /** process manager **/
    1.34  
    1.35 -  private val in_fifo = system.mk_fifo()
    1.36 -  private val out_fifo = system.mk_fifo()
    1.37 -  private def rm_fifos() { system.rm_fifo(in_fifo); system.rm_fifo(out_fifo) }
    1.38 +  private val in_fifo = Isabelle_System.mk_fifo()
    1.39 +  private val out_fifo = Isabelle_System.mk_fifo()
    1.40 +  private def rm_fifos() { Isabelle_System.rm_fifo(in_fifo); Isabelle_System.rm_fifo(out_fifo) }
    1.41  
    1.42    private val process =
    1.43      try {
    1.44        val cmdline =
    1.45 -        List(system.getenv_strict("ISABELLE_PROCESS"), "-W", in_fifo + ":" + out_fifo) ++ args
    1.46 -      new system.Managed_Process(true, cmdline: _*)
    1.47 +        List(Isabelle_System.getenv_strict("ISABELLE_PROCESS"), "-W",
    1.48 +          in_fifo + ":" + out_fifo) ++ args
    1.49 +      new Isabelle_System.Managed_Process(true, cmdline: _*)
    1.50      }
    1.51      catch { case e: IOException => rm_fifos(); throw(e) }
    1.52  
    1.53 @@ -168,8 +168,8 @@
    1.54      }
    1.55      else {
    1.56        // rendezvous
    1.57 -      val command_stream = system.fifo_output_stream(in_fifo)
    1.58 -      val message_stream = system.fifo_input_stream(out_fifo)
    1.59 +      val command_stream = Isabelle_System.fifo_output_stream(in_fifo)
    1.60 +      val message_stream = Isabelle_System.fifo_input_stream(out_fifo)
    1.61  
    1.62        standard_input = stdin_actor()
    1.63        val stdout = stdout_actor()
    1.64 @@ -341,7 +341,7 @@
    1.65  
    1.66          if (i != n) throw new Protocol_Error("bad message chunk content")
    1.67  
    1.68 -        YXML.parse_body_failsafe(YXML.decode_chars(system.symbols.decode, buf, 0, n))
    1.69 +        YXML.parse_body_failsafe(YXML.decode_chars(Isabelle_System.symbols.decode, buf, 0, n))
    1.70          //}}}
    1.71        }
    1.72