src/Pure/Tools/server.scala
changeset 67812 b123c9a007d0
parent 67811 33199d033505
child 67820 e30d6368c7c8
equal deleted inserted replaced
67811:33199d033505 67812:b123c9a007d0
   115   /* server info */
   115   /* server info */
   116 
   116 
   117   sealed case class Info(name: String, port: Int, password: String)
   117   sealed case class Info(name: String, port: Int, password: String)
   118   {
   118   {
   119     override def toString: String =
   119     override def toString: String =
   120       "server " + quote(name) + " = " + print(port, password)
   120       "server " + print_name_space(name) + "= " + print(port, password)
   121 
   121 
   122     def connection(): Connection =
   122     def connection(): Connection =
   123     {
   123     {
   124       val connection = Connection(new Socket(InetAddress.getByName("127.0.0.1"), port))
   124       val connection = Connection(new Socket(InetAddress.getByName("127.0.0.1"), port))
   125       connection.write_message(password)
   125       connection.write_message(password)
   154   }
   154   }
   155 
   155 
   156 
   156 
   157   /* per-user servers */
   157   /* per-user servers */
   158 
   158 
       
   159   def print_name_space(name: String): String =
       
   160     if (name == "") "" else quote(name) + " "
       
   161 
   159   def print(port: Int, password: String): String =
   162   def print(port: Int, password: String): String =
   160     "127.0.0.1:" + port + " (password " + quote(password) + ")"
   163     "127.0.0.1:" + port + " (password " + quote(password) + ")"
   161 
   164 
   162   object Data
   165   object Data
   163   {
   166   {
   198         db.transaction {
   201         db.transaction {
   199           find(db, name) match {
   202           find(db, name) match {
   200             case Some(server_info) => (server_info, None)
   203             case Some(server_info) => (server_info, None)
   201             case None =>
   204             case None =>
   202               if (existing_server) {
   205               if (existing_server) {
   203                 if (name == "") error("Isabelle server not running")
   206                   error("Isabelle server " + print_name_space(name) + "not running")
   204                 else error("Isabelle server " + quote(name) + " not running")
       
   205               }
   207               }
   206 
   208 
   207               val server = new Server(port)
   209               val server = new Server(port)
   208               val server_info = Info(name, server.port, server.password)
   210               val server_info = Info(name, server.port, server.password)
   209 
   211