
diff -r 2323dce4a0db -r 16fa609a62b1 src/Tools/Haskell/Haskell.thy
--- a/src/Tools/Haskell/Haskell.thy	Thu Dec 13 20:33:18 2018 +0100
+++ b/src/Tools/Haskell/Haskell.thy	Thu Dec 13 21:21:06 2018 +0100
@@ -1407,9 +1407,16 @@
 See \<^file>\<open>$ISABELLE_HOME/src/Pure/General/uuid.scala\<close>.
 -}
 
-module Isabelle.UUID (T, random, random_string, parse)
+module Isabelle.UUID (
+    T,
+    parse_string, parse_bytes,
+    string, bytes,
+    random, random_string, random_bytes
+  )
 where
 
+import Data.ByteString (ByteString)
+import qualified Data.ByteString
 import Data.UUID (UUID)
 import qualified Data.UUID as UUID
 import Data.UUID.V4 (nextRandom)
@@ -1417,14 +1424,35 @@
 
 type T = UUID
 
+
+{- parse -}
+
+parse_string :: String -> Maybe T
+parse_string = UUID.fromString
+
+parse_bytes :: ByteString -> Maybe T
+parse_bytes = UUID.fromASCIIBytes
+
+
+{- print -}
+
+string :: T -> String
+string = UUID.toString
+
+bytes :: T -> ByteString
+bytes = UUID.toASCIIBytes
+
+
+{- random id -}
+
 random :: IO T
 random = nextRandom
 
 random_string :: IO String
-random_string = UUID.toString <$> random
+random_string = string <$> random
 
-parse :: String -> Maybe T
-parse = UUID.fromString
+random_bytes :: IO ByteString
+random_bytes = bytes <$> random
 \<close>
 
 generate_file "Isabelle/Byte_Message.hs" = \<open>
@@ -1589,9 +1617,14 @@
 TCP server on localhost.
 -}
 
-module Isabelle.Server (localhost_name, localhost, publish_text, publish_stdout, server) where
+module Isabelle.Server (
+  localhost_name, localhost, publish_text, publish_stdout,
+  server
+)
+where
 
-import Control.Monad (forever)
+import Data.ByteString (ByteString)
+import Control.Monad (forever, when)
 import qualified Control.Exception as Exception
 import Network.Socket (Socket)
 import qualified Network.Socket as Socket
@@ -1599,6 +1632,7 @@
 
 import Isabelle.Library
 import qualified Isabelle.UUID as UUID
+import qualified Isabelle.Byte_Message as Byte_Message
 
 
 {- server address -}
@@ -1623,7 +1657,7 @@
 server publish handle =
   Socket.withSocketsDo $ Exception.bracket open (Socket.close . fst) (uncurry loop)
   where
-    open :: IO (Socket, UUID.T)
+    open :: IO (Socket, ByteString)
     open = do
       socket <- Socket.socket Socket.AF_INET Socket.Stream Socket.defaultProtocol
       Socket.bind socket (Socket.SockAddrInet 0 localhost)
@@ -1634,13 +1668,15 @@
       password <- UUID.random
       publish address password
 
-      return (socket, password)
+      return (socket, UUID.bytes password)
 
-    loop :: Socket -> UUID.T -> IO ()
+    loop :: Socket -> ByteString -> IO ()
     loop socket password = forever $ do
       (connection, peer) <- Socket.accept socket
       Concurrent.forkFinally
-        (handle connection)  -- FIXME check password
+        (do
+          line <- Byte_Message.read_line connection
+          when (line == Just password) $ handle connection)
         (\_ -> Socket.close connection)
       return ()
 \<close>




