# HG changeset patch
# User wenzelm
# Date 1628182433 -7200
# Node ID 17e84ae975621e25e6bee31743e1d55b2303e30c
# Parent  9e97833a0bf07e04ac7b46d0d0c54b6d6f29d1fe
tuned signature;

diff -r 9e97833a0bf0 -r 17e84ae97562 src/Tools/Haskell/Haskell.thy
--- 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