src/Doc/System/Server.thy
changeset 79724 54d0f6edfe3a
parent 79067 212c94edae2b
equal deleted inserted replaced
79723:aa77ebb2dc16 79724:54d0f6edfe3a
   489   common Isabelle timing information in seconds, usually with a precision of
   489   common Isabelle timing information in seconds, usually with a precision of
   490   three digits after the point (whole milliseconds).
   490   three digits after the point (whole milliseconds).
   491 
   491 
   492   \<^item> \<^bold>\<open>type\<close>~\<open>uuid = string\<close> refers to a Universally Unique Identifier (UUID)
   492   \<^item> \<^bold>\<open>type\<close>~\<open>uuid = string\<close> refers to a Universally Unique Identifier (UUID)
   493   as plain text.\<^footnote>\<open>See \<^url>\<open>https://www.ietf.org/rfc/rfc4122.txt\<close> and
   493   as plain text.\<^footnote>\<open>See \<^url>\<open>https://www.ietf.org/rfc/rfc4122.txt\<close> and
   494   \<^url>\<open>https://docs.oracle.com/en/java/javase/17/docs/api/java.base/java/util/UUID.html\<close>.\<close> Such
   494   \<^url>\<open>https://docs.oracle.com/en/java/javase/21/docs/api/java.base/java/util/UUID.html\<close>.\<close> Such
   495   identifiers are created as private random numbers of the server and only
   495   identifiers are created as private random numbers of the server and only
   496   revealed to the client that creates a certain resource (e.g.\ task or
   496   revealed to the client that creates a certain resource (e.g.\ task or
   497   session). A client may disclose this information for use in a different
   497   session). A client may disclose this information for use in a different
   498   client connection: this allows to share sessions between multiple
   498   client connection: this allows to share sessions between multiple
   499   connections.
   499   connections.