Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned (see also 4879d0021185);
authorwenzelm
Sun, 14 Jul 2024 15:49:26 +0200
changeset 80561 437895863e1d
parent 80560 960b866b1117
child 80562 d55cdb87f332
tuned (see also 4879d0021185);
src/Pure/PIDE/yxml.ML file | annotate | diff | comparison | revisions 
--- 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 *)
isabelle