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>\$ISABELLE_HOME/src/Pure/General/uuid.scala\. -} -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 \ generate_file "Isabelle/Byte_Message.hs" = \ @@ -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 () \