src/Pure/System/isabelle_process.scala
changeset 62556 c115e69f457f
parent 62555 fd6e64133684
child 62564 40624a9e94c4
     1.1 --- a/src/Pure/System/isabelle_process.scala	Tue Mar 08 11:18:21 2016 +0100
     1.2 +++ b/src/Pure/System/isabelle_process.scala	Tue Mar 08 14:44:11 2016 +0100
     1.3 @@ -10,21 +10,23 @@
     1.4  object Isabelle_Process
     1.5  {
     1.6    def apply(
     1.7 -    receiver: Prover.Message => Unit = Console.println(_),
     1.8 -    prover_args: List[String] = Nil): Isabelle_Process =
     1.9 +    options: Options,
    1.10 +    heap: String = "",
    1.11 +    args: List[String] = Nil,
    1.12 +    modes: List[String] = Nil,
    1.13 +    secure: Boolean = false,
    1.14 +    receiver: Prover.Receiver = Console.println(_)): Isabelle_Process =
    1.15    {
    1.16 -    val system_channel = System_Channel()
    1.17 -    val system_process =
    1.18 +    val channel = System_Channel()
    1.19 +    val process =
    1.20        try {
    1.21 -        val process =
    1.22 -          Bash.process("\"$ISABELLE_PROCESS\" -P " + File.bash_string(system_channel.server_name) +
    1.23 -            " " + File.bash_args(prover_args))
    1.24 -        process.stdin.close
    1.25 -        process
    1.26 +        ML_Process(options, heap = heap, args = args, modes = modes, secure = secure,
    1.27 +          process_socket = channel.server_name)
    1.28        }
    1.29 -      catch { case exn @ ERROR(_) => system_channel.accepted(); throw exn }
    1.30 +      catch { case exn @ ERROR(_) => channel.accepted(); throw exn }
    1.31 +    process.stdin.close
    1.32  
    1.33 -    new Isabelle_Process(receiver, system_channel, system_process)
    1.34 +    new Isabelle_Process(receiver, channel, process)
    1.35    }
    1.36  
    1.37  
    1.38 @@ -33,7 +35,7 @@
    1.39    def main(args: Array[String])
    1.40    {
    1.41      Command_Line.tool {
    1.42 -      var ml_args: List[String] = Nil
    1.43 +      var eval_args: List[String] = Nil
    1.44        var modes: List[String] = Nil
    1.45        var options = Options.init()
    1.46  
    1.47 @@ -50,8 +52,8 @@
    1.48    $ISABELLE_PATH; if it contains a slash, it is taken as literal file;
    1.49    if it is RAW_ML_SYSTEM, the initial ML heap is used.
    1.50  """,
    1.51 -        "e:" -> (arg => ml_args = ml_args ::: List("--eval", arg)),
    1.52 -        "f:" -> (arg => ml_args = ml_args ::: List("--use", arg)),
    1.53 +        "e:" -> (arg => eval_args = eval_args ::: List("--eval", arg)),
    1.54 +        "f:" -> (arg => eval_args = eval_args ::: List("--use", arg)),
    1.55          "m:" -> (arg => modes = arg :: modes),
    1.56          "o:" -> (arg => options = options + arg))
    1.57  
    1.58 @@ -62,17 +64,15 @@
    1.59            case _ => getopts.usage()
    1.60          }
    1.61  
    1.62 -      ML_Process(options, heap = heap, args = ml_args, modes = modes).
    1.63 +      ML_Process(options, heap = heap, args = eval_args ::: args.toList, modes = modes).
    1.64          result().print_stdout.rc
    1.65      }
    1.66    }
    1.67  }
    1.68  
    1.69  class Isabelle_Process private(
    1.70 -    receiver: Prover.Message => Unit,
    1.71 -    system_channel: System_Channel,
    1.72 -    system_process: Prover.System_Process)
    1.73 -  extends Prover(receiver, system_channel, system_process)
    1.74 +    receiver: Prover.Receiver, channel: System_Channel, process: Prover.System_Process)
    1.75 +  extends Prover(receiver, channel, process)
    1.76  {
    1.77    def encode(s: String): String = Symbol.encode(s)
    1.78    def decode(s: String): String = Symbol.decode(s)