# HG changeset patch
# User wenzelm
# Date 1281727993 -7200
# Node ID e753f71b6b343b2979100bdadba51480cab48e8b
# Parent  5b615a4a3a68dd47218e860c4cc24a9df1937ff9
added Isabelle_Process.input_bytes, which avoids the somewhat slow Standard_System.string_bytes (just in case someone wants to stream raw data at 250MB/s);

diff -r 5b615a4a3a68 -r e753f71b6b34 src/Pure/System/isabelle_process.scala
--- a/src/Pure/System/isabelle_process.scala	Fri Aug 13 21:30:10 2010 +0200
+++ b/src/Pure/System/isabelle_process.scala	Fri Aug 13 21:33:13 2010 +0200
@@ -373,8 +373,11 @@
 
   def input_raw(text: String): Unit = standard_input ! Input_Text(text)
 
+  def input_bytes(name: String, args: Array[Byte]*): Unit =
+    command_input ! Input_Chunks(Standard_System.string_bytes(name) :: args.toList)
+
   def input(name: String, args: String*): Unit =
-    command_input ! Input_Chunks((name :: args.toList).map(Standard_System.string_bytes))
+    input_bytes(name, args.map(Standard_System.string_bytes): _*)
 
   def close(): Unit = command_input ! Close
 }