equal
deleted
inserted
replaced
214 |
214 |
215 text \<open> |
215 text \<open> |
216 Messages are read and written as byte streams (with byte lengths), but the |
216 Messages are read and written as byte streams (with byte lengths), but the |
217 content is always interpreted as plain text in terms of the UTF-8 |
217 content is always interpreted as plain text in terms of the UTF-8 |
218 encoding.\<^footnote>\<open>See also the ``UTF-8 Everywhere Manifesto'' |
218 encoding.\<^footnote>\<open>See also the ``UTF-8 Everywhere Manifesto'' |
219 \<^url>\<open>http://utf8everywhere.org\<close>.\<close> |
219 \<^url>\<open>https://utf8everywhere.org\<close>.\<close> |
220 |
220 |
221 Note that line-endings and other formatting characters are invariant wrt. |
221 Note that line-endings and other formatting characters are invariant wrt. |
222 UTF-8 representation of text: thus implementations are free to determine the |
222 UTF-8 representation of text: thus implementations are free to determine the |
223 overall message structure before or after applying the text encoding. |
223 overall message structure before or after applying the text encoding. |
224 \<close> |
224 \<close> |