more operations;

--- a/src/Pure/Tools/server.scala	Fri Mar 09 15:24:19 2018 +0100
+++ b/src/Pure/Tools/server.scala	Fri Mar 09 15:36:27 2018 +0100
@@ -32,6 +32,19 @@
   object Reply extends Enumeration
   {
     val OK, ERROR = Value
+
+    def unapply(line: String): Option[(Reply.Value, JSON.T)] =
+    {
+      if (line == "") None
+      else {
+        val (reply, output) = split_line(line)
+        try { Some((withName(reply), JSON.parse(output, strict = false))) }
+        catch {
+          case _: NoSuchElementException => None
+          case Exn.ERROR(_) => None
+        }
+      }
+    }
   }