# HG changeset patch
# User wenzelm
# Date 1544719034 -3600
# Node ID 6439c9024dcccb92156be36ce87ba6f6af1661ff
# Parent  fe125722f7a9819e2c04ffdca3763a5ca30d683c
clarified signature;

diff -r fe125722f7a9 -r 6439c9024dcc src/Pure/General/http.scala
--- a/src/Pure/General/http.scala	Thu Dec 13 17:03:59 2018 +0100
+++ b/src/Pure/General/http.scala	Thu Dec 13 17:37:14 2018 +0100
@@ -119,8 +119,7 @@
 
   def server(handlers: List[Handler] = isabelle_resources): Server =
   {
-    val localhost = InetAddress.getByName("127.0.0.1")
-    val http_server = HttpServer.create(new InetSocketAddress(localhost, 0), 0)
+    val http_server = HttpServer.create(new InetSocketAddress(isabelle.Server.localhost, 0), 0)
     http_server.setExecutor(null)
 
     val server = new Server(http_server)
diff -r fe125722f7a9 -r 6439c9024dcc src/Pure/System/system_channel.scala
--- a/src/Pure/System/system_channel.scala	Thu Dec 13 17:03:59 2018 +0100
+++ b/src/Pure/System/system_channel.scala	Thu Dec 13 17:37:14 2018 +0100
@@ -18,9 +18,9 @@
 
 class System_Channel private
 {
-  private val server = new ServerSocket(0, 50, InetAddress.getByName("127.0.0.1"))
+  private val server = new ServerSocket(0, 50, Server.localhost)
 
-  val server_name: String = "127.0.0.1:" + server.getLocalPort
+  val server_name: String = Server.print_address(server.getLocalPort)
   override def toString: String = server_name
 
   def rendezvous(): (OutputStream, InputStream) =
diff -r fe125722f7a9 -r 6439c9024dcc src/Pure/Tools/server.scala
--- a/src/Pure/Tools/server.scala	Thu Dec 13 17:03:59 2018 +0100
+++ b/src/Pure/Tools/server.scala	Thu Dec 13 17:37:14 2018 +0100
@@ -307,16 +307,20 @@
 
   /* server info */
 
-  def print_address(port: Int): String = "127.0.0.1:" + port
+  val localhost_name: String = "127.0.0.1"
+  def localhost: InetAddress = InetAddress.getByName(localhost_name)
+
+  def print_address(port: Int): String = localhost_name + ":" + port
 
   def print(port: Int, password: String): String =
     print_address(port) + " (password " + quote(password) + ")"
 
   object Info
   {
-    private val Pattern = """server "([^"]*)" = 127\.0\.0\.1:(\d+) \(password "([^"]*)"\)""".r
+    private val Pattern =
+      ("""server "([^"]*)" = \Q""" + localhost_name + """\E:(\d+) \(password "([^"]*)"\)""").r
 
-    def unapply(s: String): Option[Info] =
+    def parse(s: String): Option[Info] =
       s match {
         case Pattern(name, Value.Int(port), password) => Some(Info(name, port, password))
         case _ => None
@@ -335,7 +339,7 @@
 
     def connection(): Connection =
     {
-      val connection = Connection(new Socket(InetAddress.getByName("127.0.0.1"), port))
+      val connection = Connection(new Socket(localhost, port))
       connection.write_message(password)
       connection
     }
@@ -508,7 +512,7 @@
 {
   server =>
 
-  private val server_socket = new ServerSocket(_port, 50, InetAddress.getByName("127.0.0.1"))
+  private val server_socket = new ServerSocket(_port, 50, Server.localhost)
 
   private val _sessions = Synchronized(Map.empty[UUID.T, Headless.Session])
   def err_session(id: UUID.T): Nothing = error("No session " + Library.single_quote(id.toString))
diff -r fe125722f7a9 -r 6439c9024dcc src/Tools/Haskell/Haskell.thy
--- a/src/Tools/Haskell/Haskell.thy	Thu Dec 13 17:03:59 2018 +0100
+++ b/src/Tools/Haskell/Haskell.thy	Thu Dec 13 17:37:14 2018 +0100
@@ -1589,7 +1589,7 @@
 TCP server on localhost.
 -}
 
-module Isabelle.Server (publish_text, publish_stdout, server) where
+module Isabelle.Server (localhost_name, localhost, publish_text, publish_stdout, server) where
 
 import Control.Monad (forever)
 import qualified Control.Exception as Exception
@@ -1603,12 +1603,12 @@
 
 {- server address -}
 
+localhost_name :: String
+localhost_name = "127.0.0.1"
+
 localhost :: Socket.HostAddress
 localhost = Socket.tupleToHostAddress (127, 0, 0, 1)
 
-localhost_name :: String
-localhost_name = "127.0.0.1"
-
 publish_text :: String -> String -> UUID.T -> String
 publish_text name address password =
   "server " ++ quote name ++ " = " ++ address ++ " (password " ++ quote (show password) ++ ")"