--- a/src/Tools/Haskell/Haskell.thy Thu Dec 13 17:01:20 2018 +0100
+++ b/src/Tools/Haskell/Haskell.thy Thu Dec 13 17:03:59 2018 +0100
@@ -1407,7 +1407,7 @@
See \<^file>\<open>$ISABELLE_HOME/src/Pure/General/uuid.scala\<close>.
-}
-module Isabelle.UUID (random, random_string, parse)
+module Isabelle.UUID (T, random, random_string, parse)
where
import Data.UUID (UUID)
@@ -1415,13 +1415,15 @@
import Data.UUID.V4 (nextRandom)
-random :: IO UUID
+type T = UUID
+
+random :: IO T
random = nextRandom
random_string :: IO String
random_string = UUID.toString <$> random
-parse :: String -> Maybe UUID
+parse :: String -> Maybe T
parse = UUID.fromString
\<close>
@@ -1587,7 +1589,7 @@
TCP server on localhost.
-}
-module Isabelle.Server (server) where
+module Isabelle.Server (publish_text, publish_stdout, server) where
import Control.Monad (forever)
import qualified Control.Exception as Exception
@@ -1595,6 +1597,11 @@
import qualified Network.Socket as Socket
import qualified Control.Concurrent as Concurrent
+import Isabelle.Library
+import qualified Isabelle.UUID as UUID
+
+
+{- server address -}
localhost :: Socket.HostAddress
localhost = Socket.tupleToHostAddress (127, 0, 0, 1)
@@ -1602,23 +1609,39 @@
localhost_name :: String
localhost_name = "127.0.0.1"
-server :: (String -> IO ()) -> (Socket -> IO ()) -> IO ()
+publish_text :: String -> String -> UUID.T -> String
+publish_text name address password =
+ "server " ++ quote name ++ " = " ++ address ++ " (password " ++ quote (show password) ++ ")"
+
+publish_stdout :: String -> String -> UUID.T -> IO ()
+publish_stdout name address password = putStrLn (publish_text name address password)
+
+
+{- server -}
+
+server :: (String -> UUID.T -> IO ()) -> (Socket -> IO ()) -> IO ()
server publish handle =
- Socket.withSocketsDo $ Exception.bracket open Socket.close loop
+ Socket.withSocketsDo $ Exception.bracket open (Socket.close . fst) (uncurry loop)
where
- open :: IO Socket
+ open :: IO (Socket, UUID.T)
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
- publish (localhost_name ++ ":" ++ show port)
- return socket
+ let address = localhost_name ++ ":" ++ show port
+ password <- UUID.random
+ publish address password
- loop :: Socket -> IO ()
- loop socket = forever $ do
+ return (socket, password)
+
+ loop :: Socket -> UUID.T -> IO ()
+ loop socket password = forever $ do
(connection, peer) <- Socket.accept socket
- Concurrent.forkFinally (handle connection) (\_ -> Socket.close connection)
+ Concurrent.forkFinally
+ (handle connection) -- FIXME check password
+ (\_ -> Socket.close connection)
return ()
\<close>