equal
deleted
inserted
replaced
352 } |
352 } |
353 |
353 |
354 |
354 |
355 /** main methods **/ |
355 /** main methods **/ |
356 |
356 |
357 def input_bytes(name: String, args: Array[Byte]*): Unit = |
357 def protocol_command_raw(name: String, args: Array[Byte]*): Unit = |
358 command_input._2 ! Input_Chunks(UTF8.string_bytes(name) :: args.toList) |
358 command_input._2 ! Input_Chunks(UTF8.string_bytes(name) :: args.toList) |
359 |
359 |
360 def input(name: String, args: String*) |
360 def protocol_command(name: String, args: String*) |
361 { |
361 { |
362 receiver(new Input(name, args.toList)) |
362 receiver(new Input(name, args.toList)) |
363 input_bytes(name, args.map(UTF8.string_bytes): _*) |
363 protocol_command_raw(name, args.map(UTF8.string_bytes): _*) |
364 } |
364 } |
365 |
365 |
366 def options(opts: Options): Unit = |
366 def options(opts: Options): Unit = |
367 input("Isabelle_Process.options", YXML.string_of_body(opts.encode)) |
367 protocol_command("Isabelle_Process.options", YXML.string_of_body(opts.encode)) |
368 } |
368 } |