diff -r d8971680b0fc -r 59ebce09ce6e src/Pure/System/isabelle_process.scala
--- a/src/Pure/System/isabelle_process.scala	Sat Sep 18 21:10:07 2010 +0200
+++ b/src/Pure/System/isabelle_process.scala	Sat Sep 18 21:33:56 2010 +0200
@@ -163,7 +163,6 @@
           //{{{
           receive {
             case Input_Text(text) =>
-              // FIXME echo input?!
               writer.write(text)
               writer.flush
             case Close =>
@@ -365,5 +364,5 @@
   def input(name: String, args: String*): Unit =
     input_bytes(name, args.map(Standard_System.string_bytes): _*)
 
-  def close(): Unit = command_input ! Close
+  def close(): Unit = { standard_input ! Close; command_input ! Close }
 }