# HG changeset patch
# User wenzelm
# Date 1628181606 -7200
# Node ID 9e97833a0bf07e04ac7b46d0d0c54b6d6f29d1fe
# Parent  d36e40f3c171a6af5d0f192e52c53f484c0739a2
clarified types: prefer Isabelle byte strings;

diff -r d36e40f3c171 -r 9e97833a0bf0 src/Tools/Haskell/Haskell.thy
--- a/src/Tools/Haskell/Haskell.thy	Thu Aug 05 12:56:08 2021 +0200
+++ b/src/Tools/Haskell/Haskell.thy	Thu Aug 05 18:40:06 2021 +0200
@@ -2628,6 +2628,8 @@
 TCP server on localhost.
 -}
 
+{-# LANGUAGE OverloadedStrings #-}
+
 module Isabelle.Server (
   localhost_name, localhost, publish_text, publish_stdout,
   server, connection
@@ -2639,8 +2641,10 @@
 import Network.Socket (Socket)
 import qualified Network.Socket as Socket
 import qualified System.IO as IO
+import qualified Data.ByteString.Char8 as Char8
 
 import Isabelle.Library
+import qualified Isabelle.Bytes as Bytes
 import Isabelle.Bytes (Bytes)
 import qualified Isabelle.UUID as UUID
 import qualified Isabelle.Byte_Message as Byte_Message
@@ -2649,24 +2653,25 @@
 
 {- server address -}
 
-localhost_name :: String
+localhost_name :: Bytes
 localhost_name = "127.0.0.1"
 
 localhost :: Socket.HostAddress
 localhost = Socket.tupleToHostAddress (127, 0, 0, 1)
 
-publish_text :: String -> String -> UUID.T -> String
+publish_text :: Bytes -> Bytes -> UUID.T -> Bytes
 publish_text name address password =
-  "server " <> quote name <> " = " <> address <> " (password " <> quote (show password) <> ")"
-
-publish_stdout :: String -> String -> UUID.T -> IO ()
+  "server " <> quote name <> " = " <> address <>
+    " (password " <> quote (make_bytes $ show password) <> ")"
+
+publish_stdout :: Bytes -> Bytes -> UUID.T -> IO ()
 publish_stdout name address password =
-  putStrLn (publish_text name address password)
+  Char8.putStrLn (Bytes.unmake $ publish_text name address password)
 
 
 {- server -}
 
-server :: (String -> UUID.T -> IO ()) -> (Socket -> IO ()) -> IO ()
+server :: (Bytes -> UUID.T -> IO ()) -> (Socket -> IO ()) -> IO ()
 server publish handle =
   Socket.withSocketsDo $ Exception.bracket open (Socket.close . fst) (uncurry loop)
   where
@@ -2677,7 +2682,7 @@
       Socket.listen server_socket 50
 
       port <- Socket.socketPort server_socket
-      let address = localhost_name <> ":" <> show port
+      let address = localhost_name <> ":" <> make_bytes (show port)
       password <- UUID.random
       publish address password