# HG changeset patch
# User wenzelm
# Date 1520606187 -3600
# Node ID fd30e767d9008dc836715b389d47c3043f9ef03e
# Parent  f801cb14a0b35033c918b2b67557d1adc161a6ff
more operations;

diff -r f801cb14a0b3 -r fd30e767d900 src/Pure/Tools/server.scala
--- 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
+        }
+      }
+    }
   }