# HG changeset patch
# User wenzelm
# Date 1544643208 -3600
# Node ID 6a901078a294758f0a8b1e13a12aace1f082b962
# Parent  ef051edd4d10b2cd971e8eac0a856859a9b47714
more Haskell operations;

diff -r ef051edd4d10 -r 6a901078a294 src/Tools/Haskell/Haskell.thy
--- a/src/Tools/Haskell/Haskell.thy	Wed Dec 12 17:34:29 2018 +0100
+++ b/src/Tools/Haskell/Haskell.thy	Wed Dec 12 20:33:28 2018 +0100
@@ -1551,4 +1551,47 @@
         Just n -> fmap trim_line . fst <$> read_block socket n
 \<close>
 
+generate_file "Isabelle/Server.hs" = \<open>
+{-  Title:      Isabelle/Server.hs
+    Author:     Makarius
+    LICENSE:    BSD 3-clause (Isabelle)
+
+TCP server on localhost.
+-}
+
+module Isabelle.Server (server) where
+
+import Control.Monad (forever)
+import qualified Control.Exception as Exception
+import Network.Socket (Socket)
+import qualified Network.Socket as Socket
+import qualified Control.Concurrent as Concurrent
+
+
+localhost :: Socket.HostAddress
+localhost = Socket.tupleToHostAddress (127, 0, 0, 1)
+
+localhost_name :: String
+localhost_name = "127.0.0.1"
+
+server :: (String -> IO ()) -> (Socket -> IO ()) -> IO ()
+server publish handle =
+  Socket.withSocketsDo $ Exception.bracket open Socket.close loop
+  where
+    open :: IO Socket
+    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
+
+    loop :: Socket -> IO ()
+    loop socket = forever $ do
+      (connection, peer) <- Socket.accept socket
+      Concurrent.forkFinally (handle connection) (\_ -> Socket.close connection)
+      return ()
+\<close>
+
 end