need to close_input before expecting threads to terminate/join;
tuned signature;

--- a/src/Pure/System/isabelle_process.scala	Tue May 29 20:38:40 2012 +0200
+++ b/src/Pure/System/isabelle_process.scala	Tue May 29 21:03:11 2012 +0200
@@ -190,6 +190,7 @@
 
       val rc = process_result.join
       system_output("process terminated")
+      close_input()
       for ((thread, _) <- List(standard_input, stdout, stderr, command_input, message))
         thread.join
       system_output("process_manager terminated")
@@ -205,7 +206,7 @@
 
   def terminate()
   {
-    close()
+    close_input()
     system_output("Terminating Isabelle process")
     terminate_process()
   }
@@ -400,5 +401,5 @@
     input_bytes(name, args.map(Standard_System.string_bytes): _*)
   }
 
-  def close(): Unit = { close(command_input); close(standard_input) }
+  def close_input(): Unit = { close(command_input); close(standard_input) }
 }