equal
deleted
inserted
replaced
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. |