diff -r f81d2a1cad69 -r e249650504f3 src/Tools/Haskell/Haskell.thy --- a/src/Tools/Haskell/Haskell.thy Wed Jul 28 15:30:40 2021 +0200 +++ b/src/Tools/Haskell/Haskell.thy Wed Jul 28 15:39:19 2021 +0200 @@ -1749,6 +1749,7 @@ and \<^file>\$ISABELLE_HOME/src/Pure/PIDE/byte_message.scala\. -} +{-# LANGUAGE OverloadedStrings #-} {-# OPTIONS_GHC -fno-warn-incomplete-patterns #-} module Isabelle.Byte_Message ( @@ -1780,11 +1781,8 @@ write :: Socket -> [ByteString] -> IO () write = Socket.sendMany -newline :: ByteString -newline = ByteString.singleton 10 - write_line :: Socket -> ByteString -> IO () -write_line socket s = write socket [s, newline] +write_line socket s = write socket [s, "\n"] {- input operations -} @@ -1834,7 +1832,7 @@ {- messages with multiple chunks (arbitrary content) -} make_header :: [Int] -> [ByteString] -make_header ns = [UTF8.encode (space_implode "," (map Value.print_int ns)), newline] +make_header ns = [UTF8.encode (space_implode "," (map Value.print_int ns)), "\n"] make_message :: [ByteString] -> [ByteString] make_message chunks = make_header (map ByteString.length chunks) <> chunks @@ -1885,7 +1883,7 @@ error ("Bad content for line message:\n" <> take 100 (UTF8.decode msg)) else (if n > 100 || ByteString.any (== 10) msg then make_header [n + 1] else []) <> - [msg, newline] + [msg, "\n"] write_line_message :: Socket -> ByteString -> IO () write_line_message socket = write socket . make_line_message