--- a/src/Tools/Haskell/Haskell.thy Thu Aug 05 18:40:06 2021 +0200
+++ b/src/Tools/Haskell/Haskell.thy Thu Aug 05 18:53:53 2021 +0200
@@ -241,6 +241,7 @@
fold, fold_rev, single, map_index, get_index, separate,
StringLike, STRING (..), TEXT (..), BYTES (..),
+ show_bytes, show_text,
proper_string, quote, space_implode, commas, commas_quote, cat_lines,
space_explode, split_lines, trim_line)
@@ -341,6 +342,12 @@
instance BYTES Lazy.Text where make_bytes = UTF8.encode . Lazy.toStrict
instance BYTES Bytes where make_bytes = id
+show_bytes :: Show a => a -> Bytes
+show_bytes = make_bytes . show
+
+show_text :: Show a => a -> Text
+show_text = make_text . show
+
{- strings -}
@@ -492,7 +499,7 @@
{- int -}
print_int :: Int -> Bytes
-print_int = make_bytes . show
+print_int = show_bytes
parse_int :: Bytes -> Maybe Int
parse_int = Read.readMaybe . make_string
@@ -2662,7 +2669,7 @@
publish_text :: Bytes -> Bytes -> UUID.T -> Bytes
publish_text name address password =
"server " <> quote name <> " = " <> address <>
- " (password " <> quote (make_bytes $ show password) <> ")"
+ " (password " <> quote (show_bytes password) <> ")"
publish_stdout :: Bytes -> Bytes -> UUID.T -> IO ()
publish_stdout name address password =
@@ -2682,7 +2689,7 @@
Socket.listen server_socket 50
port <- Socket.socketPort server_socket
- let address = localhost_name <> ":" <> make_bytes (show port)
+ let address = localhost_name <> ":" <> show_bytes port
password <- UUID.random
publish address password