src/Tools/Haskell/Haskell.thy

 module Isabelle.Bytes (
   Bytes,
   make, unmake, pack, unpack,
   empty, null, length, index, all, any,
   head, last, take, drop, isPrefixOf, isSuffixOf,
-  concat, space, spaces, char, byte, max_byte, max_char, singleton,
-  trim_line
+  concat, space, spaces, char, byte, max_byte, max_char, singleton
 )
 where
 
 import Prelude hiding (null, length, all, any, head, last, take, drop, concat)
 

   array (0, max_byte)
     [(i, make (ByteString.singleton i)) | i <- [0 .. max_byte]]
 
 singleton :: Word8 -> Bytes
 singleton b = singletons ! b
-
-trim_line :: Bytes -> Bytes
-trim_line s =
-  if n >= 2 && at (n - 2) == '\r' && at (n - 1) == '\n' then take (n - 2) s
-  else if n >= 1 && (at (n - 1) == '\r' || at (n - 1) == '\n') then take (n - 1) s
-  else s
-  where
-    n = length s
-    at = char . index s
 \<close>
 
 generate_file "Isabelle/UTF8.hs" = \<open>
 {-  Title:      Isabelle/UTF8.hs
     Author:     Makarius

 -}
 
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE TypeSynonymInstances #-}
 {-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE InstanceSigs #-}
 
 module Isabelle.Library (
   (|>), (|->), (#>), (#->),
 
   the, the_default,

 
 {- string-like interfaces -}
 
 class (IsString a, Monoid a, Eq a, Ord a) => StringLike a where
   space_explode :: Char -> a -> [a]
+  trim_line :: a -> a
 
 instance StringLike String where
+  space_explode :: Char -> String -> [String]
   space_explode c = Split.split (Split.dropDelims (Split.whenElt (== c)))
+  trim_line :: String -> String
+  trim_line s =
+    if not (null s) && Symbol.is_ascii_line_terminator (last s) then
+      case reverse s of
+        '\n' : '\r' : rest -> reverse rest
+        '\r' : rest -> reverse rest
+        '\n' : rest -> reverse rest
+        _ -> s
+    else s
 
 instance StringLike Text where
+  space_explode :: Char -> Text -> [Text]
   space_explode c str =
     if Text.null str then []
     else if Text.all (/= c) str then [str]
     else map Text.pack $ space_explode c $ Text.unpack str
+  trim_line :: Text -> Text
+  trim_line s =
+    if n >= 2 && at (n - 2) == '\r' && at (n - 1) == '\n' then Text.take (n - 2) s
+    else if n >= 1 && Symbol.is_ascii_line_terminator (at (n - 1)) then Text.take (n - 1) s
+    else s
+    where
+      n = Text.length s
+      at = Text.index s
 
 instance StringLike Lazy.Text where
+  space_explode :: Char -> Lazy.Text -> [Lazy.Text]
   space_explode c str =
     if Lazy.null str then []
     else if Lazy.all (/= c) str then [str]
     else map Lazy.pack $ space_explode c $ Lazy.unpack str
+  trim_line :: Lazy.Text -> Lazy.Text
+  trim_line = Lazy.fromStrict . trim_line . Lazy.toStrict
 
 instance StringLike Bytes where
+  space_explode :: Char -> Bytes -> [Bytes]
   space_explode c str =
     if Bytes.null str then []
     else if c > Bytes.max_char || Bytes.all (/= (Bytes.byte c)) str then [str]
     else
       explode (Bytes.unpack str)
       where
         explode rest =
           case span (/= (Bytes.byte c)) rest of
             (_, []) -> [Bytes.pack rest]
             (prfx, _ : rest') -> Bytes.pack prfx : explode rest'
+  trim_line :: Bytes -> Bytes
+  trim_line s =
+    if n >= 2 && at (n - 2) == '\r' && at (n - 1) == '\n' then Bytes.take (n - 2) s
+    else if n >= 1 && Symbol.is_ascii_line_terminator (at (n - 1)) then Bytes.take (n - 1) s
+    else s
+    where
+      n = Bytes.length s
+      at = Bytes.char . Bytes.index s
 
 class StringLike a => STRING a where make_string :: a -> String
 instance STRING String where make_string = id
 instance STRING Text where make_string = Text.unpack
 instance STRING Lazy.Text where make_string = Lazy.unpack

 split_lines :: StringLike a => a -> [a]
 split_lines = space_explode '\n'
 
 cat_lines :: StringLike a => [a] -> a
 cat_lines = space_implode "\n"
-
-trim_line :: String -> String
-trim_line line =
-  if not (null line) && Symbol.is_ascii_line_terminator (last line) then
-    case reverse line of
-      '\n' : '\r' : rest -> reverse rest
-      '\r' : rest -> reverse rest
-      '\n' : rest -> reverse rest
-      _ -> line
-  else line
 \<close>
 
 
 generate_file "Isabelle/Symbol.hs" = \<open>
 {-  Title:      Isabelle/Symbols.hs

   return (if len == n then Just msg else Nothing, len)
 
 read_line :: Socket -> IO (Maybe Bytes)
 read_line socket = read_body []
   where
-    result = Bytes.trim_line . Bytes.pack . reverse
+    result = trim_line . Bytes.pack . reverse
     read_body bs = do
       s <- Socket.recv socket 1
       case ByteString.length s of
         0 -> return (if null bs then Nothing else Just (result bs))
         1 ->

   case opt_line of
     Nothing -> return Nothing
     Just line ->
       case Value.parse_nat line of
         Nothing -> return $ Just line
-        Just n -> fmap Bytes.trim_line . fst <$> read_block socket n
+        Just n -> fmap trim_line . fst <$> read_block socket n
 
 
 read_yxml :: Socket -> IO (Maybe XML.Body)
 read_yxml socket = do
   res <- read_line_message socket