avoid empty input and its adverse effect on socket communication, e.g. output message getting "stuck" after vacuous update due to Session.update_options;

--- a/src/Pure/System/system_channel.ML	Wed Oct 16 11:48:42 2013 +0200
+++ b/src/Pure/System/system_channel.ML	Wed Oct 16 12:04:38 2013 +0200
@@ -68,7 +68,7 @@
   in
     System_Channel
      {input_line = fn () => read_line in_stream,
-      inputN = fn n => Byte.bytesToString (BinIO.inputN (in_stream, n)),
+      inputN = fn n => if n = 0 then "" else Byte.bytesToString (BinIO.inputN (in_stream, n)),
       output = fn s => BinIO.output (out_stream, Byte.stringToBytes s),
       flush = fn () => BinIO.flushOut out_stream}
   end;