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