
diff -r 12c984b7d391 -r 6d8674ffb962 src/Tools/Haskell/Haskell.thy
--- a/src/Tools/Haskell/Haskell.thy	Fri Jul 30 22:54:50 2021 +0200
+++ b/src/Tools/Haskell/Haskell.thy	Fri Jul 30 23:00:50 2021 +0200
@@ -23,7 +23,7 @@
   Bytes,
   make, unmake, pack, unpack,
   empty, null, length, index, all, any,
-  head, last, take, drop, concat,
+  head, last, take, drop, concat, trim_line
 )
 where
 
@@ -82,6 +82,15 @@
 
 concat :: [Bytes] -> Bytes
 concat = mconcat
+
+trim_line :: Bytes -> Bytes
+trim_line s =
+  if n >= 2 && at (n - 2) == 13 && at (n - 1) == 10 then take (n - 2) s
+  else if n >= 1 && (at (n - 1) == 13 || at (n - 1) == 10) then take (n - 1) s
+  else s
+  where
+    n = length s
+    at = index s
 \<close>
 
 generate_file "Isabelle/UTF8.hs" = \<open>
@@ -1840,7 +1849,7 @@
 
 module Isabelle.Byte_Message (
     write, write_line,
-    read, read_block, trim_line, read_line,
+    read, read_block, read_line,
     make_message, write_message, read_message,
     make_line_message, write_line_message, read_line_message,
     read_yxml, write_yxml
@@ -1859,7 +1868,7 @@
 import Network.Socket (Socket)
 import qualified Network.Socket.ByteString as Socket
 
-import Isabelle.Library hiding (trim_line)
+import Isabelle.Library
 import qualified Isabelle.Value as Value
 
 
@@ -1893,19 +1902,10 @@
   let len = Bytes.length msg
   return (if len == n then Just msg else Nothing, len)
 
-trim_line :: Bytes -> Bytes
-trim_line s =
-  if n >= 2 && at (n - 2) == 13 && at (n - 1) == 10 then Bytes.take (n - 2) s
-  else if n >= 1 && (at (n - 1) == 13 || at (n - 1) == 10) then Bytes.take (n - 1) s
-  else s
-  where
-    n = Bytes.length s
-    at = Bytes.index s
-
 read_line :: Socket -> IO (Maybe Bytes)
 read_line socket = read_body []
   where
-    result = trim_line . Bytes.pack . reverse
+    result = Bytes.trim_line . Bytes.pack . reverse
     read_body bs = do
       s <- Socket.recv socket 1
       case ByteString.length s of
@@ -1982,7 +1982,7 @@
     Just line ->
       case Value.parse_nat (UTF8.decode line) of
         Nothing -> return $ Just line
-        Just n -> fmap trim_line . fst <$> read_block socket n
+        Just n -> fmap Bytes.trim_line . fst <$> read_block socket n
 
 
 read_yxml :: Socket -> IO (Maybe XML.Body)




