avoid redundant XML.blob: Bytes.contents consist of larger chunks;
authorwenzelm
Sat, 31 Aug 2024 16:01:36 +0200
changeset 80794 d4c489401844
parent 80793 90f6e541e926
child 80795 5e38e8b34eb3
avoid redundant XML.blob: Bytes.contents consist of larger chunks;
src/Pure/General/bytes.ML
--- a/src/Pure/General/bytes.ML	Sat Aug 31 16:00:16 2024 +0200
+++ b/src/Pure/General/bytes.ML	Sat Aug 31 16:01:36 2024 +0200
@@ -65,7 +65,7 @@
 fun contents (Bytes {buffer, chunks, ...}) =
   rev (chunks |> not (null buffer) ? cons (compact buffer));
 
-val contents_blob = contents #> XML.blob;
+val contents_blob = contents #> map XML.Text;
 
 val content = implode o contents;