clarified signature: more uniform session_id;
authorwenzelm
Thu Mar 22 15:11:14 2018 +0100 (14 months ago)
changeset 679211722384ffd4a
parent 67920 c3c74310154e
child 67922 9e668ae81f97
clarified signature: more uniform session_id;
src/Doc/System/Server.thy
src/Pure/Tools/server_commands.scala
     1.1 --- a/src/Doc/System/Server.thy	Thu Mar 22 14:57:42 2018 +0100
     1.2 +++ b/src/Doc/System/Server.thy	Thu Mar 22 15:11:14 2018 +0100
     1.3 @@ -505,6 +505,11 @@
     1.4    and thus allows the client to control it by the \<^verbatim>\<open>cancel\<close> command. The same
     1.5    task identification is included in all messages produced by this task.
     1.6  
     1.7 +  \<^item> \<^bold>\<open>type\<close> \<open>session_id = {session_id: uuid}\<close> identifies a newly created PIDE
     1.8 +  session managed by the server. Sessions are independent of client
     1.9 +  connections and may be shared by different clients, as long as the internal
    1.10 +  session identifier is known.
    1.11 +
    1.12    \<^item> \<^bold>\<open>type\<close> \<open>node_status = {ok: bool, total: int, unprocessed: int, running:
    1.13    int, warned: int, failed: int, finished: int, consolidated: bool}\<close>
    1.14    represents a formal theory node status of the PIDE document model. Fields
    1.15 @@ -596,8 +601,8 @@
    1.16    \end{tabular}
    1.17    \<^medskip>
    1.18  
    1.19 -  The command invocation \<^verbatim>\<open>cancel {"task":\<close>~\<open>id\<close>\<^verbatim>\<open>}\<close> attempts to cancel the
    1.20 -  specified task.
    1.21 +  The command \<^verbatim>\<open>cancel {"task":\<close>~\<open>id\<close>\<^verbatim>\<open>}\<close> attempts to cancel the specified
    1.22 +  task.
    1.23  
    1.24    Cancellation is merely a hint that the client prefers an ongoing process to
    1.25    be stopped. The command always succeeds formally, but it may get ignored by
    1.26 @@ -761,14 +766,10 @@
    1.27    argument: & \<open>session_build_args \<oplus> {print_mode?: [string]}\<close> \\
    1.28    immediate result: & \<^verbatim>\<open>OK\<close> \<open>task\<close> \\
    1.29    notifications: & \<^verbatim>\<open>NOTE\<close> \<open>task \<oplus> (theory_progress | message)\<close> \\
    1.30 -  regular result: & \<^verbatim>\<open>FINISHED\<close> \<open>task \<oplus> session_start_result\<close> \\
    1.31 +  regular result: & \<^verbatim>\<open>FINISHED\<close> \<open>task \<oplus> session_id\<close> \\
    1.32    error result: & \<^verbatim>\<open>FAILED\<close> \<open>task \<oplus> error_message\<close> \\[2ex]
    1.33    \end{tabular}
    1.34  
    1.35 -  \begin{tabular}{l}
    1.36 -  \<^bold>\<open>type\<close> \<open>session_start_result = {session: string, session_id: uuid}\<close>
    1.37 -  \end{tabular}
    1.38 -
    1.39    \<^medskip>
    1.40    The \<^verbatim>\<open>session_start\<close> command starts a new Isabelle/PIDE session with
    1.41    underlying Isabelle/ML process, based on a session image that it produces on
    1.42 @@ -804,12 +805,9 @@
    1.43  subsubsection \<open>Results\<close>
    1.44  
    1.45  text \<open>
    1.46 -  The \<open>session\<close> field provides the active session name for clarity.
    1.47 -
    1.48 -  \<^medskip>
    1.49 -  The \<open>session_id\<close> field provides the internal identification of the session
    1.50 -  object within the sever process. It can remain active as long as the server
    1.51 -  is running, independently of the current client connection.
    1.52 +  The \<open>session_id\<close> provides the internal identification of the session object
    1.53 +  within the sever process. It can remain active as long as the server is
    1.54 +  running, independently of the current client connection.
    1.55  \<close>
    1.56  
    1.57  
    1.58 @@ -828,7 +826,7 @@
    1.59  
    1.60  text \<open>
    1.61    \begin{tabular}{ll}
    1.62 -  argument: & \<open>{session_id: uuid}\<close> \\
    1.63 +  argument: & \<open>session_id\<close> \\
    1.64    immediate result: & \<^verbatim>\<open>OK\<close> \<open>task\<close> \\
    1.65    regular result: & \<^verbatim>\<open>FINISHED\<close> \<open>task \<oplus> session_stop_result\<close> \\
    1.66    error result: & \<^verbatim>\<open>FAILED\<close> \<open>task \<oplus> error_message \<oplus> session_stop_result\<close> \\[2ex]
    1.67 @@ -849,8 +847,8 @@
    1.68  subsubsection \<open>Arguments\<close>
    1.69  
    1.70  text \<open>
    1.71 -  The \<open>session_id\<close> field provides the UUID originally created by the server
    1.72 -  for this session.
    1.73 +  The \<open>session_id\<close> provides the UUID originally created by the server for this
    1.74 +  session.
    1.75  \<close>
    1.76  
    1.77  
     2.1 --- a/src/Pure/Tools/server_commands.scala	Thu Mar 22 14:57:42 2018 +0100
     2.2 +++ b/src/Pure/Tools/server_commands.scala	Thu Mar 22 15:11:14 2018 +0100
     2.3 @@ -136,9 +136,8 @@
     2.4            log = log)
     2.5  
     2.6        val id = UUID()
     2.7 -      val res = JSON.Object("session" -> base_info.session, "session_id" -> id.toString)
     2.8  
     2.9 -      (res, id -> session)
    2.10 +      (JSON.Object("session_id" -> id.toString), id -> session)
    2.11      }
    2.12    }
    2.13