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
+  concat, space, spaces, char, all_char, any_char, byte, max_byte, max_char, singleton
 )
 where
 
 import Prelude hiding (null, length, all, any, head, last, take, drop, concat)
 

   if n < 64 then small_spaces ! n
   else concat ((small_spaces ! (n `mod` 64)) : replicate (n `div` 64) (small_spaces ! 64))
 
 char :: Word8 -> Char
 char = toEnum . fromEnum
+
+all_char :: (Char -> Bool) -> Bytes -> Bool
+all_char pred = all (pred . char)
+
+any_char :: (Char -> Bool) -> Bytes -> Bool
+any_char pred = any (pred . char)
 
 byte :: Char -> Word8
 byte = toEnum . fromEnum
 
 max_byte :: Word8

 
 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 if Bytes.all_char (/= c) str then [str]
     else
       explode (Bytes.unpack str)
       where
         explode rest =
           case span (/= (Bytes.byte c)) rest of

 import Prelude hiding (read)
 import Data.Maybe
 import qualified Data.ByteString as ByteString
 import qualified Isabelle.Bytes as Bytes
 import Isabelle.Bytes (Bytes)
+import qualified Isabelle.Symbol as Symbol
 import qualified Isabelle.UTF8 as UTF8
 import qualified Isabelle.XML as XML
 import qualified Isabelle.YXML as YXML
 
 import Network.Socket (Socket)

 
 -- hybrid messages: line or length+block (with content restriction)
 
 is_length :: Bytes -> Bool
 is_length msg =
-  not (Bytes.null msg) && Bytes.all (\b -> 48 <= b && b <= 57) msg
+  not (Bytes.null msg) && Bytes.all_char (\c -> '0' <= c && c <= '9') msg
 
 is_terminated :: Bytes -> Bool
 is_terminated msg =
-  not (Bytes.null msg) && (Bytes.last msg == 13 || Bytes.last msg == 10)
+  not (Bytes.null msg) && Symbol.is_ascii_line_terminator (Bytes.char $ Bytes.last msg)
 
 make_line_message :: Bytes -> [Bytes]
 make_line_message msg =
   let n = Bytes.length msg in
     if is_length msg || is_terminated msg then
       error ("Bad content for line message:\n" <> take 100 (UTF8.decode msg))
     else
-      (if n > 100 || Bytes.any (== 10) msg then make_header [n + 1] else []) <> [msg, "\n"]
+      (if n > 100 || Bytes.any_char (== '\n') msg then make_header [n + 1] else []) <> [msg, "\n"]
 
 write_line_message :: Socket -> Bytes -> IO ()
 write_line_message socket = write socket . make_line_message
 
 read_line_message :: Socket -> IO (Maybe Bytes)