src/Pure/Tools/server.scala
changeset 67796 bb2bbabf3d37
parent 67795 f8037c7e4659
child 67797 1cfc7541012e
equal deleted inserted replaced
67795:f8037c7e4659 67796:bb2bbabf3d37
   221   override def toString: String = Server.print(port, password)
   221   override def toString: String = Server.print(port, password)
   222 
   222 
   223   private def handle(connection: Server.Connection)
   223   private def handle(connection: Server.Connection)
   224   {
   224   {
   225     connection.read_line() match {
   225     connection.read_line() match {
   226       case None =>
   226       case Some(line) if line == password =>
   227       case Some(line) if line != password => connection.reply_error("Bad protocol")
   227         connection.reply_ok(JSON.empty)
   228       case _ =>
       
   229         var finished = false
   228         var finished = false
   230         while (!finished) {
   229         while (!finished) {
   231           connection.read_line() match {
   230           connection.read_line() match {
   232             case None => finished = true
   231             case None => finished = true
   233             case Some(line) if line != "" =>
   232             case Some(line) if line != "" =>
   251                   }
   250                   }
   252               }
   251               }
   253             case _ =>
   252             case _ =>
   254           }
   253           }
   255         }
   254         }
       
   255       case _ =>
   256     }
   256     }
   257   }
   257   }
   258 
   258 
   259   private lazy val server_thread: Thread =
   259   private lazy val server_thread: Thread =
   260     Standard_Thread.fork("server") {
   260     Standard_Thread.fork("server") {