# HG changeset patch # User wenzelm # Date 1381917878 -7200 # Node ID e1c275df552230e92b878a60f6f612cf6d9b9031 # Parent 18c621069bf86c084fecd0bed5713f948461746a avoid empty input and its adverse effect on socket communication, e.g. output message getting "stuck" after vacuous update due to Session.update_options; diff -r 18c621069bf8 -r e1c275df5522 src/Pure/System/system_channel.ML --- 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;