ignore empty lines;

--- a/src/Pure/Tools/server.scala	Fri Mar 09 14:26:08 2018 +0100
+++ b/src/Pure/Tools/server.scala	Fri Mar 09 14:30:13 2018 +0100
@@ -230,7 +230,7 @@
         while (!finished) {
           connection.read_line() match {
             case None => finished = true
-            case Some(line) =>
+            case Some(line) if line != "" =>
               val (cmd, input) = Server.split_line(line)
               Server.commands.get(cmd) match {
                 case None => connection.reply_error("Bad command " + quote(cmd))