# HG changeset patch
# User wenzelm
# Date 1521727062 -3600
# Node ID c3c74310154e9e6927846ed4c55b89f5968f55e5
# Parent  dd90faed43b285552f94d40542276abb168c3580
clarified signature;

diff -r dd90faed43b2 -r c3c74310154e src/Doc/System/Server.thy
--- a/src/Doc/System/Server.thy	Thu Mar 22 14:42:14 2018 +0100
+++ b/src/Doc/System/Server.thy	Thu Mar 22 14:57:42 2018 +0100
@@ -345,10 +345,10 @@
   invoke further asynchronous commands and still dispatch the resulting stream of
   asynchronous messages properly.
 
-  The synchronous command \<^verbatim>\<open>cancel\<close>~\<open>id\<close> tells the specified task to terminate
-  prematurely: usually causing a \<^verbatim>\<open>FAILED\<close> result, but this is not guaranteed:
-  the cancel event may come too late or the running process may just ignore
-  it.
+  The synchronous command \<^verbatim>\<open>cancel {"task":\<close>~\<open>id\<close>\<^verbatim>\<open>}\<close> tells the specified task
+  to terminate prematurely: usually causing a \<^verbatim>\<open>FAILED\<close> result, but this is
+  not guaranteed: the cancel event may come too late or the running process
+  may just ignore it.
 \<close>
 
 
@@ -591,12 +591,12 @@
 
 text \<open>
   \begin{tabular}{ll}
-  argument: & \<open>uuid\<close> \\
+  argument: & \<open>task\<close> \\
   regular result: & \<^verbatim>\<open>OK\<close> \\
   \end{tabular}
   \<^medskip>
 
-  The command invocation \<^verbatim>\<open>cancel "\<close>\<open>uuid\<close>\<^verbatim>\<open>"\<close> attempts to cancel the
+  The command invocation \<^verbatim>\<open>cancel {"task":\<close>~\<open>id\<close>\<^verbatim>\<open>}\<close> attempts to cancel the
   specified task.
 
   Cancellation is merely a hint that the client prefers an ongoing process to
@@ -828,7 +828,7 @@
 
 text \<open>
   \begin{tabular}{ll}
-  argument: & \<open>{session_id?: uuid}\<close> \\
+  argument: & \<open>{session_id: uuid}\<close> \\
   immediate result: & \<^verbatim>\<open>OK\<close> \<open>task\<close> \\
   regular result: & \<^verbatim>\<open>FINISHED\<close> \<open>task \<oplus> session_stop_result\<close> \\
   error result: & \<^verbatim>\<open>FAILED\<close> \<open>task \<oplus> error_message \<oplus> session_stop_result\<close> \\[2ex]
diff -r dd90faed43b2 -r c3c74310154e src/Pure/Tools/server.scala
--- a/src/Pure/Tools/server.scala	Thu Mar 22 14:42:14 2018 +0100
+++ b/src/Pure/Tools/server.scala	Thu Mar 22 14:57:42 2018 +0100
@@ -69,7 +69,8 @@
         "help" -> { case (_, ()) => table.keySet.toList.sorted },
         "echo" -> { case (_, t) => t },
         "shutdown" -> { case (context, ()) => context.server.shutdown() },
-        "cancel" -> { case (context, JSON.Value.UUID(id)) => context.cancel_task(id) },
+        "cancel" ->
+          { case (context, Server_Commands.Cancel(args)) => context.cancel_task(args.task) },
         "session_build" ->
           { case (context, Server_Commands.Session_Build(args)) =>
               context.make_task(task =>
diff -r dd90faed43b2 -r c3c74310154e src/Pure/Tools/server_commands.scala
--- a/src/Pure/Tools/server_commands.scala	Thu Mar 22 14:42:14 2018 +0100
+++ b/src/Pure/Tools/server_commands.scala	Thu Mar 22 14:57:42 2018 +0100
@@ -23,6 +23,16 @@
       case _ => None
     }
 
+  object Cancel
+  {
+    sealed case class Args(task: UUID)
+
+    def unapply(json: JSON.T): Option[Args] =
+      for { task <- JSON.uuid(json, "task") }
+      yield Args(task)
+  }
+
+
   object Session_Build
   {
     sealed case class Args(