# HG changeset patch # User wenzelm # Date 1544468402 -3600 # Node ID eaf66384cfe852e199ca847c8b16647230b8ff7e # Parent 22d4cb91ea6d08035f9e9e23cdba363e6ec78d48 clarified input_line: exclude terminator (its only use in Isabelle_Process.read_command is is unaffected, due to liberal Int.fromString); diff -r 22d4cb91ea6d -r eaf66384cfe8 src/Pure/System/system_channel.ML --- a/src/Pure/System/system_channel.ML Sun Dec 09 20:19:31 2018 +0100 +++ b/src/Pure/System/system_channel.ML Mon Dec 10 20:00:02 2018 +0100 @@ -21,7 +21,7 @@ fun input_line (System_Channel (in_stream, _)) = let - fun result cs = String.implode (rev (#"\n" :: cs)); + val result = trim_line o String.implode o rev; fun read cs = (case BinIO.input1 in_stream of NONE => if null cs then NONE else SOME (result cs)