# HG changeset patch
# User wenzelm
# Date 1720964966 -7200
# Node ID 437895863e1dc3713109e54853623542f566009c
# Parent  960b866b1117cf595a6b2dda6607db8456611049
tuned (see also 4879d0021185);

diff -r 960b866b1117 -r 437895863e1d src/Pure/PIDE/yxml.ML
--- a/src/Pure/PIDE/yxml.ML	Sun Jul 14 15:16:08 2024 +0200
+++ b/src/Pure/PIDE/yxml.ML	Sun Jul 14 15:49:26 2024 +0200
@@ -109,8 +109,7 @@
 
 val split_bytes =
   Bytes.space_explode X
-  #> filter (fn "" => false | _ => true)
-  #> map (space_explode Y);
+  #> map_filter (fn "" => NONE | s => SOME (space_explode Y s));
 
 
 (* structural errors *)