# 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>\cancel\~\id\ tells the specified task to terminate - prematurely: usually causing a \<^verbatim>\FAILED\ 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>\cancel {"task":\~\id\\<^verbatim>\}\ tells the specified task + to terminate prematurely: usually causing a \<^verbatim>\FAILED\ result, but this is + not guaranteed: the cancel event may come too late or the running process + may just ignore it. \ @@ -591,12 +591,12 @@ text \ \begin{tabular}{ll} - argument: & \uuid\ \\ + argument: & \task\ \\ regular result: & \<^verbatim>\OK\ \\ \end{tabular} \<^medskip> - The command invocation \<^verbatim>\cancel "\\uuid\\<^verbatim>\"\ attempts to cancel the + The command invocation \<^verbatim>\cancel {"task":\~\id\\<^verbatim>\}\ attempts to cancel the specified task. Cancellation is merely a hint that the client prefers an ongoing process to @@ -828,7 +828,7 @@ text \ \begin{tabular}{ll} - argument: & \{session_id?: uuid}\ \\ + argument: & \{session_id: uuid}\ \\ immediate result: & \<^verbatim>\OK\ \task\ \\ regular result: & \<^verbatim>\FINISHED\ \task \ session_stop_result\ \\ error result: & \<^verbatim>\FAILED\ \task \ error_message \ session_stop_result\ \\[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(