# HG changeset patch
# User wenzelm
# Date 1544717039 -3600
# Node ID fe125722f7a9819e2c04ffdca3763a5ca30d683c
# Parent  be142f577da6356c47d6e17a2605efd42b9b5dbc
more Haskell operations;
clarified signature;

diff -r be142f577da6 -r fe125722f7a9 src/Tools/Haskell/Haskell.thy
--- 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>