# HG changeset patch
# User wenzelm
# Date 1628275309 -7200
# Node ID 6a16f7a6719323d3e32fdca591cafdac3f73d080
# Parent  ede8a01f063a19d6b9c455e07634e8d5d6fef04f
clarified signature;

diff -r ede8a01f063a -r 6a16f7a67193 src/Tools/Haskell/Haskell.thy
--- a/src/Tools/Haskell/Haskell.thy	Fri Aug 06 20:33:59 2021 +0200
+++ b/src/Tools/Haskell/Haskell.thy	Fri Aug 06 20:41:49 2021 +0200
@@ -26,7 +26,7 @@
   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
 
@@ -112,6 +112,12 @@
 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
 
@@ -349,7 +355,7 @@
   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
@@ -2428,6 +2434,7 @@
 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
@@ -2524,11 +2531,11 @@
 
 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 =
@@ -2536,7 +2543,7 @@
     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