clarified signature;
authorwenzelm
Thu Mar 22 14:57:42 2018 +0100 (14 months ago)
changeset 67920c3c74310154e
parent 67919 dd90faed43b2
child 67921 1722384ffd4a
clarified signature;
src/Doc/System/Server.thy
src/Pure/Tools/server.scala
src/Pure/Tools/server_commands.scala
     1.1 --- a/src/Doc/System/Server.thy	Thu Mar 22 14:42:14 2018 +0100
     1.2 +++ b/src/Doc/System/Server.thy	Thu Mar 22 14:57:42 2018 +0100
     1.3 @@ -345,10 +345,10 @@
     1.4    invoke further asynchronous commands and still dispatch the resulting stream of
     1.5    asynchronous messages properly.
     1.6  
     1.7 -  The synchronous command \<^verbatim>\<open>cancel\<close>~\<open>id\<close> tells the specified task to terminate
     1.8 -  prematurely: usually causing a \<^verbatim>\<open>FAILED\<close> result, but this is not guaranteed:
     1.9 -  the cancel event may come too late or the running process may just ignore
    1.10 -  it.
    1.11 +  The synchronous command \<^verbatim>\<open>cancel {"task":\<close>~\<open>id\<close>\<^verbatim>\<open>}\<close> tells the specified task
    1.12 +  to terminate prematurely: usually causing a \<^verbatim>\<open>FAILED\<close> result, but this is
    1.13 +  not guaranteed: the cancel event may come too late or the running process
    1.14 +  may just ignore it.
    1.15  \<close>
    1.16  
    1.17  
    1.18 @@ -591,12 +591,12 @@
    1.19  
    1.20  text \<open>
    1.21    \begin{tabular}{ll}
    1.22 -  argument: & \<open>uuid\<close> \\
    1.23 +  argument: & \<open>task\<close> \\
    1.24    regular result: & \<^verbatim>\<open>OK\<close> \\
    1.25    \end{tabular}
    1.26    \<^medskip>
    1.27  
    1.28 -  The command invocation \<^verbatim>\<open>cancel "\<close>\<open>uuid\<close>\<^verbatim>\<open>"\<close> attempts to cancel the
    1.29 +  The command invocation \<^verbatim>\<open>cancel {"task":\<close>~\<open>id\<close>\<^verbatim>\<open>}\<close> attempts to cancel the
    1.30    specified task.
    1.31  
    1.32    Cancellation is merely a hint that the client prefers an ongoing process to
    1.33 @@ -828,7 +828,7 @@
    1.34  
    1.35  text \<open>
    1.36    \begin{tabular}{ll}
    1.37 -  argument: & \<open>{session_id?: uuid}\<close> \\
    1.38 +  argument: & \<open>{session_id: uuid}\<close> \\
    1.39    immediate result: & \<^verbatim>\<open>OK\<close> \<open>task\<close> \\
    1.40    regular result: & \<^verbatim>\<open>FINISHED\<close> \<open>task \<oplus> session_stop_result\<close> \\
    1.41    error result: & \<^verbatim>\<open>FAILED\<close> \<open>task \<oplus> error_message \<oplus> session_stop_result\<close> \\[2ex]
     2.1 --- a/src/Pure/Tools/server.scala	Thu Mar 22 14:42:14 2018 +0100
     2.2 +++ b/src/Pure/Tools/server.scala	Thu Mar 22 14:57:42 2018 +0100
     2.3 @@ -69,7 +69,8 @@
     2.4          "help" -> { case (_, ()) => table.keySet.toList.sorted },
     2.5          "echo" -> { case (_, t) => t },
     2.6          "shutdown" -> { case (context, ()) => context.server.shutdown() },
     2.7 -        "cancel" -> { case (context, JSON.Value.UUID(id)) => context.cancel_task(id) },
     2.8 +        "cancel" ->
     2.9 +          { case (context, Server_Commands.Cancel(args)) => context.cancel_task(args.task) },
    2.10          "session_build" ->
    2.11            { case (context, Server_Commands.Session_Build(args)) =>
    2.12                context.make_task(task =>
     3.1 --- a/src/Pure/Tools/server_commands.scala	Thu Mar 22 14:42:14 2018 +0100
     3.2 +++ b/src/Pure/Tools/server_commands.scala	Thu Mar 22 14:57:42 2018 +0100
     3.3 @@ -23,6 +23,16 @@
     3.4        case _ => None
     3.5      }
     3.6  
     3.7 +  object Cancel
     3.8 +  {
     3.9 +    sealed case class Args(task: UUID)
    3.10 +
    3.11 +    def unapply(json: JSON.T): Option[Args] =
    3.12 +      for { task <- JSON.uuid(json, "task") }
    3.13 +      yield Args(task)
    3.14 +  }
    3.15 +
    3.16 +
    3.17    object Session_Build
    3.18    {
    3.19      sealed case class Args(