src/Tools/Haskell/Haskell.thy

 Universally unique identifiers.
 
 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)
 
 
 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
-
-parse :: String -> Maybe T
-parse = UUID.fromString
+random_string = string <$> random
+
+random_bytes :: IO ByteString
+random_bytes = bytes <$> random
 \<close>
 
 generate_file "Isabelle/Byte_Message.hs" = \<open>
 {-  Title:      Isabelle/Byte_Message.hs
     Author:     Makarius

     LICENSE:    BSD 3-clause (Isabelle)
 
 TCP server on localhost.
 -}
 
-module Isabelle.Server (localhost_name, localhost, publish_text, publish_stdout, server) where
-
-import Control.Monad (forever)
+module Isabelle.Server (
+  localhost_name, localhost, publish_text, publish_stdout,
+  server
+)
+where
+
+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
 import qualified Control.Concurrent as Concurrent
 
 import Isabelle.Library
 import qualified Isabelle.UUID as UUID
+import qualified Isabelle.Byte_Message as Byte_Message
 
 
 {- server address -}
 
 localhost_name :: String

 
 server :: (String -> UUID.T -> IO ()) -> (Socket -> IO ()) -> IO ()
 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)
       Socket.listen socket 50
 
       port <- Socket.socketPort socket
       let address = localhost_name ++ ":" ++ show port
       password <- UUID.random
       publish address password
 
-      return (socket, password)
-
-    loop :: Socket -> UUID.T -> IO ()
+      return (socket, UUID.bytes password)
+
+    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>
 
 end